(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* [] (**********************************************************************) (* Various externalisation functions *) let insert_delimiters e = function | None -> e | Some sc -> CDelimiters (dummy_loc,sc,e) let insert_pat_delimiters e = function | None -> e | Some sc -> CPatDelimiters (dummy_loc,sc,e) (**********************************************************************) (* conversion of references *) let ids_of_ctxt ctxt = Array.to_list (Array.map (function c -> match kind_of_term c with | Var id -> id | _ -> error "Termast: arbitrary substitution of references not yet implemented") ctxt) let idopt_of_name = function | Name id -> Some id | Anonymous -> None let extern_evar loc n = (* msgerrnl (str "Warning: existential variable turned into meta-variable during externalization"); CPatVar (loc,(false,make_ident "META" (Some n))) *) CEvar (loc,n) let raw_string_of_ref = function | ConstRef kn -> "CONST("^(string_of_kn kn)^")" | IndRef (kn,i) -> "IND("^(string_of_kn kn)^","^(string_of_int i)^")" | ConstructRef ((kn,i),j) -> "CONSTRUCT("^ (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")" | VarRef id -> "SECVAR("^(string_of_id id)^")" (* v7->v8 translation *) let name_app f = function | Name id -> Name (f id) | Anonymous -> Anonymous let rec translate_ident_string = function (* translate keyword *) | ("at" | "IF" | "forall" | "fun" | "match" | "fix" | "cofix" | "for" | "let" | "if" | "then" | "else" | "return" | "mod" | "where" | "exists" | "exists2" | "using" as s) -> let s' = s^"_" in msgerrnl (str ("Warning: '"^ s^"' is now a keyword; it has been translated to '"^s'^"'")); s' (* Le conflit est en fait surtout avec Eval dans Definition et c'est gere dans Ppconstrnew | "eval" as s -> let s' = s^"_" in msgerrnl (str ("Warning: '"^ s^"' is a conflicting ident; it has been translated to '"^s'^"'")); s' *) (* avoid _ *) | "_" -> msgerrnl (str "Warning: '_' is no longer an ident; it has been translated to 'x_'"); "x_" (* avoid @ *) | s when String.contains s '@' -> let n = String.index s '@' in translate_ident_string (String.sub s 0 n ^ "'at'" ^ String.sub s (n+1) (String.length s -n-1)) | s -> s let translate_ident id = id_of_string (translate_ident_string (string_of_id id)) let is_coq_root d = let d = repr_dirpath d in d <> [] & string_of_id (list_last d) = "Coq" let is_dir dir s = let d = repr_dirpath dir in d <> [] & string_of_id (List.hd d) = s let is_module m = is_dir (Lib.library_dp()) m let bp = ["BinPos"] let bz = ["BinInt"] let bn = ["BinNat"] let pn = ["nat"] let zc = ["Zcompare"] let lo = ["Logic"] let da = ["Datatypes"] let zabs = ["Zabs"] let zo = ["Zorder"] let zn = ["Znat"] let wz = ["Wf_Z"] let mu = ["Mult"] let pl = ["Plus"] let mi = ["Minus"] let le = ["Le"] let gt = ["Gt"] let lt = ["Lt"] let be = ["Between"] let bo = ["Bool"] let c dir = let d = repr_dirpath dir in if d = [] then [] else [string_of_id (List.hd d)] let translation_table = [ (* ZArith *) "double_moins_un", (bp,"Pdouble_minus_one"); "double_moins_deux", (bp,"Pdouble_minus_two"); "is_double_moins_un", (bp,"Psucc_o_double_minus_one_eq_xO"); "double_moins_un_add_un_xI", (bp,"Pdouble_minus_one_o_succ_eq_xI"); "add_un_Zs", (bz,"Zpos_succ_morphism"); "entier", (bn,"N"); "entier_of_Z", (bz,"Zabs_N"); "Z_of_entier", (bz,"Z_of_N"); "SUPERIEUR", (da,"Gt"); "EGAL", (da,"Eq"); "INFERIEUR", (da,"Lt"); "add", (bp,"Pplus"); "add_carry", (bp,"Pplus_carry"); "add_assoc", (bp,"Pplus_assoc"); "add_sym", (bp,"Pplus_comm"); "add_x_x", (bp,"Pplus_diag"); "add_carry_add", (bp,"Pplus_carry_plus"); "simpl_add_r", (bp,"Pplus_reg_r"); "simpl_add_l", (bp,"Pplus_reg_l"); "simpl_add_carry_r", (bp,"Pplus_carry_reg_r"); "simpl_add_carry_l", (bp,"Pplus_carry_reg_l"); "simpl_times_r", (bp,"Pmult_reg_r"); "simpl_times_l", (bp,"Pmult_reg_l"); (* "xO_xI_add_double_moins_un", (bp,"xO_xI_plus_double_minus_one"); *) "double_moins_un_plus_xO_double_moins_un", (bp,"Pdouble_minus_one_plus_xO_double_minus_one"); "add_xI_double_moins_un", (bp,"Pplus_xI_double_minus_one"); "add_xO_double_moins_un", (bp,"Pplus_xO_double_minus_one"); "iter_pos_add", (bp,"iter_pos_plus"); "add_no_neutral", (bp,"Pplus_no_neutral"); "add_carry_not_add_un", (bp,"Pplus_carry_no_neutral"); "times_add_distr", (bp,"Pmult_plus_distr_l"); "times_add_distr_l", (bp,"Pmult_plus_distr_r"); "times_true_sub_distr", (bp,"Pmult_minus_distr_l"); "times_sym", (bp,"Pmult_comm"); "times_assoc", (bp,"Pmult_assoc"); "times_convert", (bp,"nat_of_P_mult_morphism"); "true_sub", (bp,"Pminus"); "times_x_1", (bp,"Pmult_1_r"); "times_x_double", (bp,"Pmult_xO_permute_r"); (* Changer en Pmult_xO_distrib_r_reverse *) "times_x_double_plus_one", (bp,"Pmult_xI_permute_r"); (* Changer ? *) "times_discr_xO_xI", (bp,"Pmult_xI_mult_xO_discr"); "times_discr_xO", (bp,"Pmult_xO_discr"); "times_one_inversion_l", (bp,"Pmult_1_inversion_l"); "true_sub_convert", (bp,"nat_of_P_minus_morphism"); "compare_true_sub_right", (bp,"Pcompare_minus_r"); "compare_true_sub_left", (bp,"Pcompare_minus_l"); "sub_add", (bp,"Pplus_minus" (* similar to le_plus_minus in Arith *)); "sub_add_one", (bp,"Ppred_succ"); "add_sub_one", (bp,"Psucc_pred"); "add_un", (bp,"Psucc"); "add_un_discr", (bp,"Psucc_discr"); "add_un_not_un", (bp,"Psucc_not_one"); "add_un_inj", (bp,"Psucc_inj"); "xI_add_un_xO", (bp,"xI_succ_xO"); "ZL12", (bp,"Pplus_one_succ_r"); "ZL12bis", (bp,"Pplus_one_succ_l"); "ZL13", (bp,"Pplus_carry_spec"); (* Changer en Pplus_succ_distrib_r_reverse ? *) "ZL14", (bp,"Pplus_succ_permute_r"); (* Changer en Plus_succ_distrib_l_reverse *) "ZL14bis", (bp,"Pplus_succ_permute_l"); "sub_un", (bp,"Ppred"); "sub_pos", (bp,"Pminus_mask"); "sub_pos_x_x", (bp,"Pminus_mask_diag"); (*"sub_pos_x_x", (bp,"Pminus_mask_diag");*) "sub_pos_SUPERIEUR", (bp,"Pminus_mask_Gt"); "sub_neg", (bp,"Pminus_mask_carry"); "Zdiv2_pos", (bp,"Pdiv2"); "Pdiv2", (["Zbinary"],"Zdiv2_ge_compat"); "ZERO", (bz,"Z0"); "POS", (bz,"Zpos"); "NEG", (bz,"Zneg"); "Nul", (bn,"N0"); "Pos", (bn,"Npos"); "Un_suivi_de", (bn,"Ndouble_plus_one"); "Zero_suivi_de", (bn,"Ndouble"); "Un_suivi_de_mask", (bp,"Pdouble_plus_one_mask"); "Zero_suivi_de_mask", (bp,"Pdouble_mask"); "ZS", (bp,"double_eq_zero_inversion"); "US", (bp,"double_plus_one_zero_discr"); "USH", (bp,"double_plus_one_eq_one_inversion"); "ZSH", (bp,"double_eq_one_discr"); "ZPminus_add_un_permute", (bz,"ZPminus_succ_permute"); "ZPminus_add_un_permute_Zopp", (bz,"ZPminus_succ_permute_opp"); "ZPminus_double_moins_un_xO_add_un", (bz,"ZPminus_double_minus_one_xO_succ"); "ZL1", (bp,"xO_succ_permute"); (* ?? *) "Zplus_assoc_r", (bz,"Zplus_assoc_reverse"); "Zplus_sym", (bz,"Zplus_comm"); "Zero_left", (bz,"Zplus_0_l"); "Zero_right", (bz,"Zplus_0_r"); "Zplus_n_O", (bz,"Zplus_0_r_reverse"); "Zplus_unit_left", (bz,"Zplus_0_simpl_l"); "Zplus_unit_right", (bz,"Zplus_0_simpl_l_reverse"); "Zplus_Zopp_expand", (bz,"Zplus_opp_expand"); "Zn_Sn", (bz,"Zsucc_discr"); "Zs", (bz,"Zsucc"); "Psucc_Zs", (bz,"Zpos_succ_permute"); "Zs_pred", (bz,"Zsucc_pred"); "Zpred_Sn", (bz,"Zpred_succ"); "Zminus_n_O", (bz,"Zminus_0_l_reverse"); "Zminus_n_n", (bz,"Zminus_diag_reverse"); "Zminus_Sn_m", (bz,"Zminus_succ_l"); "Zeq_Zminus", (bz,"Zeq_minus"); "Zminus_Zeq", (bz,"Zminus_eq"); "Zplus_minus", (bz,"Zplus_minus_eq"); "Zminus_plus", (bz,"Zminus_plus"); "Zminus_plus_simpl", (bz,"Zminus_plus_simpl_l_reverse"); "Zminus_Zplus_compatible", (bz,"Zminus_plus_simpl_r"); "Zle_plus_minus", (bz,"Zplus_minus"); "Zopp_Zplus", (bz,"Zopp_plus_distr"); "Zopp_Zopp", (bz,"Zopp_involutive"); "Zopp_NEG", (bz,"Zopp_neg"); "Zopp_Zdouble", (bz,"Zopp_double"); "Zopp_Zdouble_plus_one", (bz,"Zopp_double_plus_one"); "Zopp_Zdouble_minus_one", (bz,"Zopp_double_minus_one"); "Zplus_inverse_r", (bz,"Zplus_opp_r"); "Zplus_inverse_l", (bz,"Zplus_opp_l"); "Zplus_S_n", (bz,"Zplus_succ_l"); "Zplus_n_Sm", (bz,"Zplus_succ_r"); "Zplus_Snm_nSm", (bz,"Zplus_succ_comm"); "Zmult_assoc_r", (bz,"Zmult_assoc_reverse"); "Zmult_sym", (bz,"Zmult_comm"); "Zmult_eq", (bz,"Zmult_integral_l"); "Zmult_zero", (bz,"Zmult_integral"); "Zero_mult_left", (bz,"Zmult_0_l"); "Zero_mult_right", (bz,"Zmult_0_r"); "Zmult_1_n", (bz,"Zmult_1_l"); "Zmult_n_1", (bz,"Zmult_1_r"); "Zmult_n_O", (bz,"Zmult_0_r_reverse"); "Zopp_one", (bz,"Zopp_eq_mult_neg_1"); "Zopp_Zmult", (bz,"Zopp_mult_distr_l_reverse"); "Zopp_Zmult_r", (bz,"Zopp_mult_distr_r"); "Zopp_Zmult_l", (bz,"Zopp_mult_distr_l"); "Zmult_Zopp_Zopp", (bz,"Zmult_opp_opp"); "Zmult_Zopp_left", (bz,"Zmult_opp_comm"); "Zmult_Zplus_distr", (bz,"Zmult_plus_distr_r"); "Zmult_plus_distr", (bz,"Zmult_plus_distr_r"); "Zmult_Zminus_distr_r", (bz,"Zmult_minus_distr_l"); "Zmult_Zminus_distr_l", (bz,"Zmult_minus_distr_r"); "Zcompare_Zplus_compatible", (zc,"Zcompare_plus_compat"); "Zcompare_Zplus_compatible2", (zc,"Zplus_compare_compat"); "Zcompare_Zmult_compatible", (zc,"Zcompare_mult_compat"); "inject_nat", (bz,"Z_of_nat"); "inject_nat_complete", (wz,"Z_of_nat_complete"); "inject_nat_complete_inf", (wz,"Z_of_nat_complete_inf"); "inject_nat_prop", (wz,"Z_of_nat_prop"); "inject_nat_set", (wz,"Z_of_nat_set"); "convert", (bp,"nat_of_P"); "anti_convert", (bp,"P_of_succ_nat"); "positive_to_nat", (bp,"Pmult_nat"); "Zopp_intro", (bz,"Zopp_inj"); "plus_iter_add", (bp,"plus_iter_eq_plus"); "compare", (bp,"Pcompare"); "iter_convert", (["Zmisc"],"iter_nat_of_P"); "ZLSI", (bp,"Pcompare_Gt_Lt"); "ZLIS", (bp,"Pcompare_Lt_Gt"); "ZLII", (bp,"Pcompare_Lt_Lt"); "ZLSS", (bp,"Pcompare_Gt_Gt"); (* Pnat *) "convert_intro", (pn,"nat_of_P_inj"); "convert_add", (pn,"nat_of_P_plus_morphism"); "convert_add_un", (pn,"Pmult_nat_succ_morphism"); "cvt_add_un", (pn,"nat_of_P_succ_morphism"); "convert_add_carry", (pn,"Pmult_nat_plus_carry_morphism"); "compare_convert_O", (pn,"lt_O_nat_of_P"); "add_verif", (pn,"Pmult_nat_l_plus_morphism"); "ZL2", (pn,"Pmult_nat_r_plus_morphism"); "compare_positive_to_nat_O", (pn,"le_Pmult_nat"); (* Trop spécifique ? "ZL6", (pn,"Pmult_nat_plus_shift_morphism"); *) "ZL15", (pn,"Pplus_carry_pred_eq_plus"); "cvt_carry", (pn,"nat_of_P_plus_carry_morphism"); "compare_convert1", (pn,"Pcompare_not_Eq"); "compare_convert_INFERIEUR", (pn,"nat_of_P_lt_Lt_compare_morphism"); "compare_convert_SUPERIEUR", (pn,"nat_of_P_gt_Gt_compare_morphism"); "compare_convert_EGAL", (pn,"Pcompare_Eq_eq"); "convert_compare_INFERIEUR", (pn,"nat_of_P_lt_Lt_compare_complement_morphism"); "convert_compare_SUPERIEUR", (pn,"nat_of_P_gt_Gt_compare_complement_morphism"); "convert_compare_EGAL", (pn,"Pcompare_refl"); "bij1", (pn,"nat_of_P_o_P_of_succ_nat_eq_succ"); "bij2", (pn,"P_of_succ_nat_o_nat_of_P_eq_succ"); "bij3", (pn,"pred_o_P_of_succ_nat_o_nat_of_P_eq_id"); (* Zcompare *) "Zcompare_EGAL", (zc,"Zcompare_Eq_iff_eq"); "Zcompare_EGAL_eq", (zc,"Zcompare_Eq_eq"); "Zcompare_x_x", (zc,"Zcompare_refl"); "Zcompare_et_un", (zc,"Zcompare_Gt_not_Lt"); "Zcompare_trans_SUPERIEUR", (zc,"Zcompare_Gt_trans"); "Zcompare_n_S", (zc,"Zcompare_succ_compat"); "SUPERIEUR_POS", (zc,"Zcompare_Gt_spec"); "Zcompare_ANTISYM", (zc,"Zcompare_Gt_Lt_antisym"); "Zcompare_Zs_SUPERIEUR", (zc,"Zcompare_succ_Gt"); "Zcompare_Zopp", (zc,"Zcompare_opp"); "POS_inject", (zn,"Zpos_eq_Z_of_nat_o_nat_of_P"); "absolu", (bz,"Zabs_nat"); "absolu_lt", (zabs,"Zabs_nat_lt" (* "Zabs_nat_lt_morphism_pos" ? *)); "Zeq_add_S", (bz,"Zsucc_inj"); "Znot_eq_S", (bz,"Zsucc_inj_contrapositive"); "Zeq_S", (bz,"Zsucc_eq_compat"); "Zsimpl_plus_l", (bz,"Zplus_reg_l"); "Zplus_simpl", (bz,"Zplus_eq_compat"); "POS_gt_ZERO", (zo,"Zgt_pos_0"); "ZERO_le_POS", (zo,"Zle_0_pos"); "ZERO_le_inj", (zo,"Zle_0_nat"); "NEG_lt_ZERO", (zo,"Zlt_neg_0"); "Zlt_ZERO_pred_le_ZERO", (zo,"Zlt_0_le_0_pred"); "POS_xI", (bz,"Zpos_xI"); "POS_xO", (bz,"Zpos_xO"); "NEG_xI", (bz,"Zneg_xI"); "NEG_xO", (bz,"Zneg_xO"); "POS_add", (bz,"Zpos_plus_distr"); "NEG_add", (bz,"Zneg_plus_distr"); (* Z Orders *) "not_Zge", (zo,"Znot_ge_lt"); "not_Zlt", (zo,"Znot_lt_ge"); "not_Zle", (zo,"Znot_le_gt"); "not_Zgt", (zo,"Znot_gt_le"); "Zgt_not_sym", (zo,"Zgt_asym"); "Zlt_not_sym", (zo,"Zlt_asym"); "Zlt_n_n", (zo,"Zlt_irrefl"); "Zgt_antirefl", (zo,"Zgt_irrefl"); "Zgt_reg_l", (zo,"Zplus_gt_compat_l"); "Zgt_reg_r", (zo,"Zplus_gt_compat_r"); "Zlt_reg_l", (zo,"Zplus_lt_compat_l"); "Zlt_reg_r", (zo,"Zplus_lt_compat_r"); "Zle_reg_l", (zo,"Zplus_le_compat_l"); "Zle_reg_r", (zo,"Zplus_le_compat_r"); "Zlt_le_reg", (zo,"Zplus_lt_le_compat"); "Zle_lt_reg", (zo,"Zplus_le_lt_compat"); "Zle_plus_plus", (zo,"Zplus_le_compat"); "Zlt_Zplus", (zo,"Zplus_lt_compat"); "Zle_O_plus", (zo,"Zplus_le_0_compat"); "Zle_mult_simpl", (zo,"Zmult_le_reg_r"); "Zge_mult_simpl", (zo,"Zmult_ge_reg_r"); "Zgt_mult_simpl", (zo,"Zmult_gt_reg_r"); "Zsimpl_gt_plus_l", (zo,"Zplus_gt_reg_l"); "Zsimpl_gt_plus_r", (zo,"Zplus_gt_reg_r"); "Zsimpl_le_plus_l", (zo,"Zplus_le_reg_l"); "Zsimpl_le_plus_r", (zo,"Zplus_le_reg_r"); "Zsimpl_lt_plus_l", (zo,"Zplus_lt_reg_l"); "Zsimpl_lt_plus_r", (zo,"Zplus_lt_reg_r"); "Zlt_Zmult_right2", (zo,"Zmult_gt_0_lt_reg_r"); "Zlt_Zmult_right", (zo,"Zmult_gt_0_lt_compat_r"); "Zle_Zmult_right2", (zo,"Zmult_gt_0_le_reg_r"); "Zle_Zmult_right", (zo,"Zmult_gt_0_le_compat_r"); "Zgt_Zmult_right", (zo,"Zmult_gt_compat_r"); "Zgt_Zmult_left", (zo,"Zmult_gt_compat_l"); "Zlt_Zmult_left", (zo,"Zmult_gt_0_lt_compat_l"); "Zcompare_Zmult_right", (zc,"Zmult_compare_compat_r"); "Zcompare_Zmult_left", (zc,"Zmult_compare_compat_l"); "Zplus_Zmult_2", (bz,"Zplus_diag_eq_mult_2"); "Zmult_Sm_n", (bz,"Zmult_succ_l_reverse"); "Zmult_n_Sm", (bz,"Zmult_succ_r_reverse"); "Zmult_le", (zo,"Zmult_le_0_reg_r"); "Zmult_reg_left", (bz,"Zmult_reg_l"); "Zmult_reg_right", (bz,"Zmult_reg_r"); "Zle_ZERO_mult", (zo,"Zmult_le_0_compat"); "Zgt_ZERO_mult", (zo,"Zmult_gt_0_compat"); "Zle_mult", (zo,"Zmult_gt_0_le_0_compat"); "Zmult_lt", (zo,"Zmult_gt_0_lt_0_reg_r"); "Zmult_gt", (zo,"Zmult_gt_0_reg_l"); "Zle_Zmult_pos_right", (zo,"Zmult_le_compat_r"); "Zle_Zmult_pos_left", (zo,"Zmult_le_compat_l"); "Zge_Zmult_pos_right", (zo,"Zmult_ge_compat_r"); "Zge_Zmult_pos_left", (zo,"Zmult_ge_compat_l"); "Zge_Zmult_pos_compat", (zo,"Zmult_ge_compat"); "Zlt_Zcompare", (zo,"Zlt_compare"); "Zle_Zcompare", (zo,"Zle_compare"); "Zgt_Zcompare", (zo,"Zgt_compare"); "Zge_Zcompare", (zo,"Zge_compare"); (* ex-IntMap *) "convert_xH", (pn,"nat_of_P_xH"); "convert_xO", (pn,"nat_of_P_xO"); "convert_xI", (pn,"nat_of_P_xI"); "positive_to_nat_mult", (pn,"Pmult_nat_mult_permute"); "positive_to_nat_2", (pn,"Pmult_nat_2_mult_2_permute"); "positive_to_nat_4", (pn,"Pmult_nat_4_mult_2_permute"); (* ZArith and Arith orders *) "Zle_refl", (zo,"Zeq_le"); "Zle_n", (zo,"Zle_refl"); "Zle_trans_S", (zo,"Zle_succ_le"); "Zgt_trans_S", (zo,"Zge_trans_succ"); "Zgt_S", (zo,"Zgt_succ_gt_or_eq"); "Zle_Sn_n", (zo,"Znot_le_succ"); "Zlt_n_Sn", (zo,"Zlt_succ"); "Zlt_S", (zo,"Zlt_lt_succ"); "Zlt_n_S", (zo,"Zsucc_lt_compat"); "Zle_n_S", (zo,"Zsucc_le_compat"); "Zgt_n_S", (zo,"Zsucc_gt_compat"); "Zlt_S_n", (zo,"Zsucc_lt_reg"); "Zgt_S_n", (zo,"Zsucc_gt_reg"); "Zle_S_n", (zo,"Zsucc_le_reg"); "Zle_0_plus", (zo,"Zplus_le_0_compat"); "Zgt_Sn_n", (zo,"Zgt_succ"); "Zgt_le_S", (zo,"Zgt_le_succ"); "Zgt_S_le", (zo,"Zgt_succ_le"); "Zle_S_gt", (zo,"Zlt_succ_gt"); "Zle_gt_S", (zo,"Zlt_gt_succ"); "Zgt_pred", (zo,"Zgt_succ_pred"); "Zlt_pred", (zo,"Zlt_succ_pred"); "Zgt0_le_pred", (zo,"Zgt_0_le_0_pred"); "Z_O_1", (zo,"Zlt_0_1"); "Zle_NEG_POS", (zo,"Zle_neg_pos"); "Zle_n_Sn", (zo,"Zle_succ"); "Zle_pred_n", (zo,"Zle_pred"); "Zlt_pred_n_n", (zo,"Zlt_pred"); "Zlt_le_S", (zo,"Zlt_le_succ"); "Zlt_n_Sm_le", (zo,"Zlt_succ_le"); "Zle_lt_n_Sm", (zo,"Zle_lt_succ"); "Zle_le_S", (zo,"Zle_le_succ"); "Zlt_minus", (zo,"Zlt_minus_simpl_swap"); "le_trans_S", (le,"le_Sn_le"); (* Znumtheory *) "Zdivide_Zmod", ([],"Zdivide_mod"); "Zmod_Zdivide", ([],"Zmod_divide"); "Zdivide_mult_left", ([],"Zmult_divide_compat_l"); "Zdivide_mult_right", ([],"Zmult_divide_compat_r"); "Zdivide_opp", ([],"Zdivide_opp_r"); "Zdivide_opp_rev", ([],"Zdivide_opp_r_rev"); "Zdivide_opp_left", ([],"Zdivide_opp_l"); "Zdivide_opp_left_rev", ([],"Zdivide_opp_l_rev"); "Zdivide_right", ([],"Zdivide_mult_r"); "Zdivide_left", ([],"Zdivide_mult_l"); "Zdivide_plus", ([],"Zdivide_plus_r"); "Zdivide_minus", ([],"Zdivide_minus_l"); "Zdivide_a_ab", ([],"Zdivide_factor_r"); "Zdivide_a_ba", ([],"Zdivide_factor_l"); (* Arith *) (* Peano.v "plus_n_O", ("plus_0_r_reverse"); "plus_O_n", ("plus_0_l"); *) "plus_assoc_l", (pl,"plus_assoc"); "plus_assoc_r", (pl,"plus_assoc_reverse"); "plus_sym", (pl,"plus_comm"); "mult_sym", (mu,"mult_comm"); "max_sym", (["Max"],"max_comm"); "min_sym", (["Min"],"min_comm"); "gt_not_sym", (gt,"gt_asym"); "lt_not_sym", (lt,"lt_asym"); "gt_antirefl", (gt,"gt_irrefl"); "lt_n_n", (lt,"lt_irrefl"); (* Trop utilisé dans CoqBook | "le_n" -> "le_refl"*) "simpl_plus_l", (pl,"plus_reg_l"); "simpl_plus_r", (pl,"plus_reg_r"); "fact_growing", (["Factorial"],"fact_le"); "mult_assoc_l", (mu,"mult_assoc"); "mult_assoc_r", (mu,"mult_assoc_reverse"); "mult_plus_distr", (mu,"mult_plus_distr_r"); "mult_plus_distr_r", (mu,"mult_plus_distr_l"); "mult_minus_distr", (mu,"mult_minus_distr_r"); "mult_1_n", (mu,"mult_1_l"); "mult_n_1", (mu,"mult_1_r"); (* Peano.v "mult_n_O", ("mult_O_r_reverse"); "mult_n_Sm", ("mult_S_r_reverse"); *) "mult_le", (mu,"mult_le_compat_l"); "le_mult_right", (mu,"mult_le_compat_r"); "le_mult_mult", (mu,"mult_le_compat"); "mult_lt", (mu,"mult_S_lt_compat_l"); "lt_mult_right", (mu,"mult_lt_compat_r"); "mult_le_conv_1", (mu,"mult_S_le_reg_l"); "exists", (be,"exists_between"); "IHexists", ([],"IHexists_between"); (* Peano.v "pred_Sn", ("pred_S"); *) "inj_minus_aux", (mi,"not_le_minus_0"); "minus_x_x", (mi,"minus_diag"); "minus_plus_simpl", (mi,"minus_plus_simpl_l_reverse"); "gt_reg_l", (gt,"plus_gt_compat_l"); "le_reg_l", (pl,"plus_le_compat_l"); "le_reg_r", (pl,"plus_le_compat_r"); "lt_reg_l", (pl,"plus_lt_compat_l"); "lt_reg_r", (pl,"plus_lt_compat_r"); "le_plus_plus", (pl,"plus_le_compat"); "le_lt_plus_plus", (pl,"plus_le_lt_compat"); "lt_le_plus_plus", (pl,"plus_lt_le_compat"); "lt_plus_plus", (pl,"plus_lt_compat"); "plus_simpl_l", (pl,"plus_reg_l"); "simpl_gt_plus_l", (pl,"plus_gt_reg_l"); "simpl_le_plus_l", (pl,"plus_le_reg_l"); "simpl_lt_plus_l", (pl,"plus_lt_reg_l"); (* Noms sur le principe de ceux de Z "le_n_S", ("S_le_compat"); "le_n_Sn", ("le_S"); (*"le_O_n", ("??" *)); "le_pred_n", ("le_pred"); "le_trans_S", ("le_S_le"); "le_S_n", ("S_le_reg"); "le_Sn_O", ("not_le_S_O"); "le_Sn_n", ("not_le_S"); *) (* Init *) "IF", (lo,"IF_then_else"); (* Lists *) "idempot_rev", (["List"],"rev_involutive"); "forall", (["Streams"],"HereAndFurther"); (* Bool *) "orb_sym", (bo,"orb_comm"); "andb_sym", (bo,"andb_comm"); (* Ring *) "SR_plus_sym", (["Ring_theory"],"SR_plus_comm"); "SR_mult_sym", (["Ring_theory"],"SR_mult_comm"); "Th_plus_sym", (["Ring_theory"],"Th_plus_comm"); "Th_mul_sym", (["Ring_theory"],"Th_mult_comm"); "SSR_plus_sym", (["Setoid_ring_theory"],"SSR_plus_comm"); "SSR_mult_sym", (["Setoid_ring_theory"],"SSR_mult_comm"); "STh_plus_sym", (["Setoid_ring_theory"],"STh_plus_comm"); "STh_mul_sym", (["Setoid_ring_theory"],"STh_mult_comm"); (* Reals *) (* "Rabsolu", ("Rabs"); "Rabsolu_pos_lt", ("Rabs_pos_lt"); "Rabsolu_no_R0", ("Rabs_no_R0"); "Rabsolu_Rabsolu", ("Rabs_Rabs"); "Rabsolu_mult", ("Rabs_mult"); "Rabsolu_triang", ("Rabs_triang"); "Rabsolu_Ropp", ("Rabs_Ropp"); "Rabsolu_right", ("Rabs_right"); ... "case_Rabsolu", ("case_Rabs"); "Pow_Rabsolu", ("Pow_Rabs"); ... *) (* Raxioms *) "complet", ([],"completeness"); "complet_weak", ([],"completeness_weak"); "Rle_sym1", ([],"Rle_ge"); "Rmin_sym", ([],"Rmin_comm"); "Rplus_sym", ([],"Rplus_comm"); "Rmult_sym", ([],"Rmult_comm"); "Rsqr_times", ([],"Rsqr_mult"); "sqrt_times", ([],"sqrt_mult"); "Rmult_1l", ([],"Rmult_1_l"); "Rplus_Ol", ([],"Rplus_0_l"); "Rplus_Ropp_r", ([],"Rplus_opp_r"); "Rmult_Rplus_distr", ([],"Rmult_plus_distr_l"); "Rlt_antisym", ([],"Rlt_asym"); (* RIneq *) "Rlt_antirefl", ([],"Rlt_irrefl"); "Rlt_compatibility", ([],"Rplus_lt_compat_l"); "Rgt_plus_plus_r", ([],"Rplus_gt_compat_l"); "Rgt_r_plus_plus", ([],"Rplus_gt_reg_l"); "Rge_plus_plus_r", ([],"Rplus_ge_compat_l"); "Rge_r_plus_plus", ([],"Rplus_ge_reg_l"); (* Si on en change un, il faut changer tous les autres R*_monotony *) "Rlt_monotony", ([],"Rmult_lt_compat_l"); "Rlt_monotony_r", ([],"Rmult_lt_compat_r"); "Rlt_monotony_contra", ([],"Rmult_lt_reg_l"); (*"Rlt_monotony_rev", ([],"Rmult_lt_reg_l");*) "Rlt_anti_monotony", ([],"Rmult_lt_gt_compat_neg_l"); "Rle_monotony", ([],"Rmult_le_compat_l"); "Rle_monotony_r", ([],"Rmult_le_compat_r"); "Rle_monotony_contra", ([],"Rmult_le_reg_l"); "Rle_anti_monotony1", ([],"Rmult_le_compat_neg_l"); "Rle_anti_monotony", ([],"Rmult_le_ge_compat_neg_l"); "Rge_monotony", ([],"Rmult_ge_compat_r"); "Rge_ge_eq", ([],"Rge_antisym"); (* Le reste de RIneq *) "imp_not_Req", ([],"Rlt_dichotomy_converse"); "Req_EM", ([],"Req_dec"); "total_order", ([],"Rtotal_order"); "not_Req", ([],"Rdichotomy"); (* "Rlt_le" -> c dir,"Rlt_le_weak" ? *) "not_Rle", ([],"Rnot_le_lt"); "not_Rge", ([],"Rnot_ge_lt"); "Rlt_le_not", ([],"Rlt_not_le"); "Rle_not", ([],"Rgt_not_le"); "Rle_not_lt", ([],"Rle_not_lt"); "Rlt_ge_not", ([],"Rlt_not_ge"); "eq_Rle", ([],"Req_le"); "eq_Rge", ([],"Req_ge"); "eq_Rle_sym", ([],"Req_le_sym"); "eq_Rge_sym", ([],"Req_ge_sym"); (* "Rle_le_eq" -> ? x<=y/\y<=x <-> x=y *) "Rlt_rew", ([],"Rlt_eq_compat"); "total_order_Rlt", ([],"Rlt_dec"); "total_order_Rle", ([],"Rle_dec"); "total_order_Rgt", ([],"Rgt_dec"); "total_order_Rge", ([],"Rge_dec"); "total_order_Rlt_Rle", ([],"Rlt_le_dec"); (* "Rle_or_lt" -> c dir,"Rle_or_lt"*) "total_order_Rle_Rlt_eq", ([],"Rle_lt_or_eq_dec"); (* "inser_trans_R" -> c dir,"Rle_lt_inser_trans" ?*) (* "Rplus_ne" -> c dir,"Rplus_0_r_l" ? *) "Rplus_Or", ([],"Rplus_0_r"); "Rplus_Ropp_l", ([],"Rplus_opp_l"); "Rplus_Ropp", ([],"Rplus_opp_r_uniq"); "Rplus_plus_r", ([],"Rplus_eq_compat_l"); "r_Rplus_plus", ([],"Rplus_eq_reg_l"); "Rplus_ne_i", ([],"Rplus_0_r_uniq"); "Rmult_Or", ([],"Rmult_0_r"); "Rmult_Ol", ([],"Rmult_0_l"); (* "Rmult_ne" -> c dir,"Rmult_1_l_r" ? *) "Rmult_1r", ([],"Rmult_1_r"); "Rmult_mult_r", ([],"Rmult_eq_compat_l"); "r_Rmult_mult", ([],"Rmult_eq_reg_l"); "without_div_Od", ([],"Rmult_integral"); "without_div_Oi", ([],"Rmult_eq_0_compat"); "without_div_Oi1", ([],"Rmult_eq_0_compat_r"); "without_div_Oi2", ([],"Rmult_eq_0_compat_l"); "without_div_O_contr", ([],"Rmult_neq_0_reg"); "mult_non_zero", ([],"Rmult_integral_contrapositive"); "Rmult_Rplus_distrl", ([],"Rmult_plus_distr_r"); "Rsqr_O", ([],"Rsqr_0"); "Rsqr_r_R0", ([],"Rsqr_0_uniq"); "eq_Ropp", ([],"Ropp_eq_compat"); "Ropp_O", ([],"Ropp_0"); "eq_RoppO", ([],"Ropp_eq_0_compat"); "Ropp_Ropp", ([],"Ropp_involutive"); "Ropp_neq", ([],"Ropp_neq_0_compat"); "Ropp_distr1", ([],"Ropp_plus_distr"); "Ropp_mul1", ([],"Ropp_mult_distr_l_reverse"); "Ropp_mul2", ([],"Rmult_opp_opp"); "Ropp_mul3", ([],"Ropp_mult_distr_r_reverse"); "minus_R0", ([],"Rminus_0_r"); "Rminus_Ropp", ([],"Rminus_0_l"); "Ropp_distr2", ([],"Ropp_minus_distr"); "Ropp_distr3", ([],"Ropp_minus_distr'"); "eq_Rminus", ([],"Rminus_diag_eq"); "Rminus_eq", ([],"Rminus_diag_uniq"); "Rminus_eq_right", ([],"Rminus_diag_uniq_sym"); "Rplus_Rminus", ([],"Rplus_minus"); (* "Rminus_eq_contra", ([],"Rminus_diag_neq"); "Rminus_not_eq", ([],"Rminus_neq_diag_sym"); "Rminus_not_eq_right" -> ? *) "Rminus_distr", ([],"Rmult_minus_distr_l"); "Rinv_R1", ([],"Rinv_1"); "Rinv_neq_R0", ([],"Rinv_neq_0_compat"); "Rinv_Rinv", ([],"Rinv_involutive"); "Rinv_Rmult", ([],"Rinv_mult_distr"); "Ropp_Rinv", ([],"Ropp_inv_permute"); (* "Rinv_r_simpl_r" -> OK ? *) (* "Rinv_r_simpl_l" -> OK ? *) (* "Rinv_r_simpl_m" -> OK ? *) "Rinv_Rmult_simpl", ([],"Rinv_mult_simpl"); (* ? *) "Rlt_compatibility_r", ([],"Rplus_lt_compat_r"); "Rlt_anti_compatibility", ([],"Rplus_lt_reg_r"); "Rle_compatibility", ([],"Rplus_le_compat_l"); "Rle_compatibility_r", ([],"Rplus_le_compat_r"); "Rle_anti_compatibility", ([],"Rplus_le_reg_l"); (* "sum_inequa_Rle_lt" -> ? *) "Rplus_lt", ([],"Rplus_lt_compat"); "Rplus_le", ([],"Rplus_le_compat"); "Rplus_lt_le_lt", ([],"Rplus_lt_le_compat"); "Rplus_le_lt_lt", ([],"Rplus_le_lt_compat"); "Rgt_Ropp", ([],"Ropp_gt_lt_contravar"); "Rlt_Ropp", ([],"Ropp_lt_gt_contravar"); "Ropp_Rlt", ([],"Ropp_lt_cancel"); (* ?? *) "Rlt_Ropp1", ([],"Ropp_lt_contravar"); "Rle_Ropp", ([],"Ropp_le_ge_contravar"); "Ropp_Rle", ([],"Ropp_le_cancel"); "Rle_Ropp1", ([],"Ropp_le_contravar"); "Rge_Ropp", ([],"Ropp_ge_le_contravar"); "Rlt_RO_Ropp", ([],"Ropp_0_lt_gt_contravar"); "Rgt_RO_Ropp", ([],"Ropp_0_gt_lt_contravar"); "Rle_RO_Ropp", ([],"Ropp_0_le_ge_contravar"); "Rge_RO_Ropp", ([],"Ropp_0_ge_le_contravar"); (* ... cf plus haut pour les lemmes intermediaires *) "Rle_Rmult_comp", ([],"Rmult_le_compat"); (* Expliciter que la contrainte est r2>0 dans r1 "Rle_minus" -> "Rminus_lt" -> "Rminus_le" -> "tech_Rplus" -> *) "pos_Rsqr", ([],"Rle_0_sqr"); "pos_Rsqr1", ([],"Rlt_0_sqr"); "Rlt_R0_R1", ([],"Rlt_0_1"); "Rle_R0_R1", ([],"Rle_0_1"); "Rlt_Rinv", ([],"Rinv_0_lt_compat"); "Rlt_Rinv2", ([],"Rinv_lt_0_compat"); "Rinv_lt", ([],"Rinv_lt_contravar"); "Rlt_Rinv_R1", ([],"Rinv_1_lt_contravar"); "Rlt_not_ge", ([],"Rnot_lt_ge"); "Rgt_not_le", ([],"Rnot_gt_le"); (* "Rgt_ge" -> "Rgt_ge_weak" ? *) "Rlt_sym", ([],"Rlt_gt_iff"); (* | "Rle_sym1" -> c dir,"Rle_ge" OK *) "Rle_sym2", ([],"Rge_le"); "Rle_sym", ([],"Rle_ge_iff"); (* "Rge_gt_trans" -> OK "Rgt_ge_trans" -> OK "Rgt_trans" -> OK "Rge_trans" -> OK *) "Rgt_RoppO", ([],"Ropp_lt_gt_0_contravar"); "Rlt_RoppO", ([],"Ropp_gt_lt_0_contravar"); "Rlt_r_plus_R1", ([],"Rle_lt_0_plus_1"); "Rlt_r_r_plus_R1", ([],"Rlt_plus_1"); (* "tech_Rgt_minus" -> ? *) (* OK, cf plus haut "Rgt_r_plus_plus", ([],"Rplus_gt_reg_l"); "Rgt_plus_plus_r", ([],"Rplus_gt_compat_l"); "Rge_plus_plus_r", ([],"Rplus_ge_compat_l"); "Rge_r_plus_plus", ([],"Rplus_ge_reg_l"); "Rge_monotony" -> *) (* "Rgt_minus" -> "minus_Rgt" -> "Rge_minus" -> "minus_Rge" -> *) "Rmult_gt", ([],"Rmult_gt_0_compat"); "Rmult_lt_pos", ([],"Rmult_lt_0_compat"); (* lt_0 ou 0_lt ?? *) "Rplus_eq_R0_l", ([],"Rplus_eq_0_l"); (* ? *) "Rplus_eq_R0", ([],"Rplus_eq_R0"); "Rplus_Rsr_eq_R0_l", ([],"Rplus_sqr_eq_0_l"); "Rplus_Rsr_eq_R0", ([],"Rplus_sqr_eq_0"); (* "S_INR" -> "S_O_plus_INR" -> "plus_INR" -> "minus_INR" -> "mult_INR" -> "lt_INR_0" -> "lt_INR" -> "INR_lt_1" -> "INR_pos" -> "pos_INR" -> "INR_lt" -> "le_INR" -> "not_INR_O" -> "not_O_INR" -> "not_nm_INR" -> "INR_eq" -> "INR_le" -> "not_1_INR" -> "IZN" -> "INR_IZR_INZ" -> "plus_IZR_NEG_POS" -> "plus_IZR" -> "mult_IZR" -> "Ropp_Ropp_IZR" -> "Z_R_minus" -> "lt_O_IZR" -> "lt_IZR" -> "eq_IZR_R0" -> "eq_IZR" -> "not_O_IZR" -> "le_O_IZR" -> "le_IZR" -> "le_IZR_R1" -> "IZR_ge" -> "IZR_le" -> "IZR_lt" -> "one_IZR_lt1" -> "one_IZR_r_R1" -> "single_z_r_R1" -> "tech_single_z_r_R1" -> "prod_neq_R0" -> "Rmult_le_pos" -> "double" -> "double_var" -> *) "gt0_plus_gt0_is_gt0", ([],"Rplus_lt_0_compat"); "ge0_plus_gt0_is_gt0", ([],"Rplus_le_lt_0_compat"); "gt0_plus_ge0_is_gt0", ([],"Rplus_lt_le_0_compat"); "ge0_plus_ge0_is_ge0", ([],"Rplus_le_le_0_compat"); (* "plus_le_is_le" -> ? "plus_lt_is_lt" -> ? *) "Rmult_lt2", ([],"Rmult_le_0_lt_compat"); (* "Rge_ge_eq" -> c dir,"Rge_antisym" OK *) ] let translate_v7_string dir s = try let d,s' = List.assoc s translation_table in (if d=[] then c dir else d),s' with Not_found -> (* Special cases *) match s with (* Init *) | "relation" when is_module "Datatypes" or is_dir dir "Datatypes" -> da,"comparison" | "Op" when is_module "Datatypes" or is_dir dir "Datatypes" -> da,"CompOpp" (* BinPos *) | "times" when not (is_module "Mapfold") -> bp,"Pmult" (* Reals *) | s when String.length s >= 7 & (String.sub s 0 7 = "Rabsolu") -> c dir, "Rabs"^(String.sub s 7 (String.length s - 7)) | s when String.length s >= 7 & (String.sub s (String.length s - 7) 7 = "Rabsolu") -> c dir, "R"^(String.sub s 0 (String.length s - 7))^"abs" | s when String.length s >= 7 & let s' = String.sub s 0 7 in (s' = "unicite" or s' = "unicity") -> c dir, "uniqueness"^(String.sub s 7 (String.length s - 7)) | s when String.length s >= 3 & let s' = String.sub s 0 3 in s' = "gcd" -> c dir, "Zis_gcd"^(String.sub s 3 (String.length s - 3)) (* Default *) | x -> [],x let id_of_v7_string s = id_of_string (if !Options.v7 then s else snd (translate_v7_string empty_dirpath s)) let v7_to_v8_dir_id dir id = if Options.do_translate() then let s = string_of_id id in let dir',s = if (is_coq_root (Lib.library_dp()) or is_coq_root dir) then translate_v7_string dir s else [], s in dir',id_of_string (translate_ident_string s) else [],id let v7_to_v8_id id = snd (v7_to_v8_dir_id empty_dirpath id) let short_names = List.map (fun x -> snd (snd x)) translation_table let is_new_name s = Options.do_translate () & (List.mem s short_names or s = "comparison" or s = "CompOpp" or s = "Pmult" or (String.length s >= 4 & String.sub s 0 4 = "Rabs") or (String.length s >= 4 & String.sub s (String.length s - 3) 3 = "abs" & s.[0] = 'R') or (String.length s >= 10 & String.sub s 0 10 = "uniqueness")) let v7_to_v8_dir fulldir dir = if Options.do_translate () & dir <> empty_dirpath then let update s = let l = List.map string_of_id (repr_dirpath dir) in make_dirpath (List.map id_of_string (s :: List.tl l)) in let l = List.map string_of_id (repr_dirpath fulldir) in if l = [ "List"; "Lists"; "Coq" ] then update "MonoList" else if l = [ "PolyList"; "Lists"; "Coq" ] then update "List" else dir else dir let shortest_qualid_of_v7_global ctx ref = let fulldir,_ = repr_path (sp_of_global ref) in let dir,id = repr_qualid (shortest_qualid_of_global ctx ref) in let dir',id = v7_to_v8_dir_id fulldir id in let dir'' = if dir' = [] then (* A name that is not renamed *) if dir = empty_dirpath & is_new_name (string_of_id id) then (* An unqualified name that is not renamed but which coincides *) (* with a new name: force qualification unless it is a variable *) if fulldir <> empty_dirpath & not (is_coq_root fulldir) then make_dirpath [List.hd (repr_dirpath fulldir)] else empty_dirpath else v7_to_v8_dir fulldir dir else (* A stdlib name that has been renamed *) try let d,_ = repr_path (Nametab.full_name_cci (make_short_qualid id)) in if not (is_coq_root d) then (* The user has defined id, then we qualify the new name *) v7_to_v8_dir fulldir (make_dirpath (List.map id_of_string dir')) else empty_dirpath with Not_found -> v7_to_v8_dir fulldir dir in make_qualid dir'' id let extern_reference loc vars r = try Qualid (loc,shortest_qualid_of_v7_global vars r) with Not_found -> (* happens in debugger *) Ident (loc,id_of_string (raw_string_of_ref r)) (************************************************************************) (* Equality up to location (useful for translator v8) *) let rec check_same_pattern p1 p2 = match p1, p2 with | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 -> check_same_pattern a1 a2 | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 -> List.iter2 check_same_pattern a1 a2 | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> () | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> () | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 -> check_same_pattern e1 e2 | _ -> failwith "not same pattern" let check_same_ref r1 r2 = match r1,r2 with | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> () | Ident(_,i1), Ident(_,i2) when i1=i2 -> () | _ -> failwith "not same ref" let rec check_same_type ty1 ty2 = match ty1, ty2 with | CRef r1, CRef r2 -> check_same_ref r1 r2 | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 -> List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) -> if id1<>id2 || i1<>i2 then failwith "not same fix"; check_same_fix_binder bl1 bl2; check_same_type a1 a2; check_same_type b1 b2) fl1 fl2 | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 -> List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) -> if id1<>id2 then failwith "not same fix"; check_same_fix_binder bl1 bl2; check_same_type a1 a2; check_same_type b1 b2) fl1 fl2 | CArrow(_,a1,b1), CArrow(_,a2,b2) -> check_same_type a1 a2; check_same_type b1 b2 | CProdN(_,bl1,a1), CProdN(_,bl2,a2) -> List.iter2 check_same_binder bl1 bl2; check_same_type a1 a2 | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> List.iter2 check_same_binder bl1 bl2; check_same_type a1 a2 | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 -> check_same_type a1 a2; check_same_type b1 b2 | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 -> List.iter2 check_same_type al1 al2 | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) -> check_same_type e1 e2; List.iter2 (fun (a1,e1) (a2,e2) -> if e1<>e2 then failwith "not same expl"; check_same_type a1 a2) al1 al2 | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) -> List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> List.iter2 check_same_pattern pl1 pl2; check_same_type r1 r2) brl1 brl2 | COrderedCase(_,_,_,a1,bl1), COrderedCase(_,_,_,a2,bl2) -> check_same_type a1 a2; List.iter2 check_same_type bl1 bl2 | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () | CSort(_,s1), CSort(_,s2) when s1=s2 -> () | CCast(_,a1,b1), CCast(_,a2,b2) -> check_same_type a1 a2; check_same_type b1 b2 | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 -> List.iter2 check_same_type e1 e2 | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> () | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 -> check_same_type e1 e2 | _ when ty1=ty2 -> () | _ -> failwith "not same type" and check_same_binder (nal1,e1) (nal2,e2) = List.iter2 (fun (_,na1) (_,na2) -> if na1<>na2 then failwith "not same name") nal1 nal2; check_same_type e1 e2 and check_same_fix_binder bl1 bl2 = List.iter2 (fun b1 b2 -> match b1,b2 with LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) -> check_same_binder (nal1,ty1) (nal2,ty2) | LocalRawDef(na1,def1), LocalRawDef(na2,def2) -> check_same_binder ([na1],def1) ([na2],def2) | _ -> failwith "not same binder") bl1 bl2 let same c d = try check_same_type c d; true with _ -> false (* Idem for rawconstr *) let option_iter2 f o1 o2 = match o1, o2 with Some o1, Some o2 -> f o1 o2 | None, None -> () | _ -> failwith "option" let array_iter2 f v1 v2 = List.iter2 f (Array.to_list v1) (Array.to_list v2) let rec same_patt p1 p2 = match p1, p2 with PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar" | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) -> if c1<>c2 || al1 <> al2 then failwith "PatCstr"; List.iter2 same_patt pl1 pl2 | _ -> failwith "same_patt" let rec same_raw c d = match c,d with | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef" | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar" | REvar(_,e1,a1), REvar(_,e2,a2) -> if e1 <> e2 then failwith "REvar"; option_iter2(List.iter2 same_raw) a1 a2 | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar" | RApp(_,f1,a1), RApp(_,f2,a2) -> List.iter2 same_raw (f1::a1) (f2::a2) | RLambda(_,na1,t1,m1), RLambda(_,na2,t2,m2) -> if na1 <> na2 then failwith "RLambda"; same_raw t1 t2; same_raw m1 m2 | RProd(_,na1,t1,m1), RProd(_,na2,t2,m2) -> if na1 <> na2 then failwith "RProd"; same_raw t1 t2; same_raw m1 m2 | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) -> if na1 <> na2 then failwith "RLetIn"; same_raw t1 t2; same_raw m1 m2 | RCases(_,_,c1,b1), RCases(_,_,c2,b2) -> List.iter2 (fun (t1,{contents=(al1,oind1)}) (t2,{contents=(al2,oind2)}) -> same_raw t1 t2; if al1 <> al2 then failwith "RCases"; option_iter2(fun (_,i1,nl1) (_,i2,nl2) -> if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2; List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) -> List.iter2 same_patt pl1 pl2; same_raw b1 b2) b1 b2 | ROrderedCase(_,_,_,c1,v1,_), ROrderedCase(_,_,_,c2,v2,_) -> same_raw c1 c2; array_iter2 same_raw v1 v2 | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) -> if nl1<>nl2 then failwith "RLetTuple"; same_raw b1 b2; same_raw c1 c2 | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) -> same_raw b1 b2; same_raw t1 t2; same_raw e1 e2 | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) -> if fk1 <> fk2 || na1 <> na2 then failwith "RRec"; array_iter2 (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) -> if na1<>na2 then failwith "RRec"; option_iter2 same_raw bd1 bd2; same_raw ty1 ty2)) bl1 bl2; array_iter2 same_raw ty1 ty2; array_iter2 same_raw def1 def2 | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort" | RHole _, _ -> () | _, RHole _ -> () | RCast(_,c1,_),r2 -> same_raw c1 r2 | r1, RCast(_,c2,_) -> same_raw r1 c2 | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic" | _ -> failwith "same_raw" let same_rawconstr c d = try same_raw c d; true with Failure _ | Invalid_argument _ -> false (**********************************************************************) (* mapping patterns to cases_pattern_expr *) let make_current_scopes (scopt,scopes) = option_fold_right push_scope scopt scopes let has_curly_brackets ntn = String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or String.sub ntn (String.length ntn - 6) 6 = " { _ }" or string_string_contains ntn " { _ } ") let rec wildcards ntn n = if n = String.length ntn then [] else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l and spaces ntn n = if n = String.length ntn then [] else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1) let expand_curly_brackets make_ntn ntn l = let ntn' = ref ntn in let rec expand_ntn i = function | [] -> [] | a::l -> let a' = let p = List.nth (wildcards !ntn' 0) i - 2 in if p>=0 & p+5 <= String.length !ntn' & String.sub !ntn' p 5 = "{ _ }" then begin ntn' := String.sub !ntn' 0 p ^ "_" ^ String.sub !ntn' (p+5) (String.length !ntn' -p-5); make_ntn "{ _ }" [a] end else a in a' :: expand_ntn (i+1) l in let l = expand_ntn 0 l in (* side effect *) make_ntn !ntn' l let make_notation loc ntn l = if has_curly_brackets ntn then expand_curly_brackets (fun n l -> CNotation (loc,n,l)) ntn l else match ntn,l with (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) | "- _", [CNumeral(_,Bignat.POS p)] -> CNotation (loc,ntn,[CNotation(loc,"( _ )",l)]) | _ -> CNotation (loc,ntn,l) let make_pat_notation loc ntn l = if has_curly_brackets ntn then expand_curly_brackets (fun n l -> CPatNotation (loc,n,l)) ntn l else match ntn,l with (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) | "- _", [CPatNumeral(_,Bignat.POS p)] -> CPatNotation (loc,ntn,[CPatNotation(loc,"( _ )",l)]) | _ -> CPatNotation (loc,ntn,l) (* let rec cases_pattern_expr_of_constr_expr = function | CRef r -> CPatAtom (dummy_loc,Some r) | CHole loc -> CPatAtom (loc,None) | CApp (loc,(proj,CRef c),l) when proj = None -> let l,e = List.split l in if not (List.for_all ((=) None) e) then anomaly "Unexpected explicitation in pattern"; CPatCstr (loc,c,List.map cases_pattern_expr_of_constr_expr l) | CNotation (loc,ntn,l) -> CPatNotation (loc,ntn,List.map cases_pattern_expr_of_constr_expr l) | CNumeral (loc,n) -> CPatNumeral (loc,n) | CDelimiters (loc,s,e) -> CPatDelimiters (loc,s,cases_pattern_expr_of_constr_expr e) | _ -> anomaly "Constrextern: not a pattern" let rec rawconstr_of_cases_pattern = function | PatVar (loc,Name id) -> RVar (loc,id) | PatVar (loc,Anonymous) -> RHole (loc,InternalHole) | PatCstr (loc,(ind,_ as c),args,_) -> let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in let params = list_tabulate (fun _ -> RHole (loc,InternalHole)) nparams in let args = params @ List.map rawconstr_of_cases_pattern args in let f = RRef (loc,ConstructRef c) in if args = [] then f else RApp (loc,f,args) *) let bind_env sigma var v = try let vvar = List.assoc var sigma in if v=vvar then sigma else raise No_match with Not_found -> (* TODO: handle the case of multiple occs in different scopes *) (var,v)::sigma let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1 | PatVar (_,Anonymous), AHole _ -> sigma | a, AHole _ when not(Options.do_translate()) -> sigma | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ -> let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in let l2 = match a2 with | ARef (ConstructRef r2) when r1 = r2 -> [] | AApp (ARef (ConstructRef r2),l2) when r1 = r2 -> l2 | _ -> raise No_match in if List.length l2 <> nparams + List.length args1 then raise No_match else let (p2,args2) = list_chop nparams l2 in (* All parameters must be _ *) List.iter (function AHole _ -> () | _ -> raise No_match) p2; List.fold_left2 (match_cases_pattern metas) sigma args1 args2 | _ -> raise No_match let match_aconstr_cases_pattern c (metas_scl,pat) = let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in (* Reorder canonically the substitution *) let find x subst = try List.assoc x subst with Not_found -> anomaly "match_aconstr_cases_pattern" in List.map (fun (x,scl) -> (find x subst,scl)) metas_scl (* Better to use extern_rawconstr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope scopes vars pat = try if !Options.raw_print or !print_no_symbol then raise No_match; let (sc,n) = Symbols.uninterp_cases_numeral pat in match Symbols.availability_of_numeral sc (make_current_scopes scopes) with | None -> raise No_match | Some key -> let loc = pattern_loc pat in insert_pat_delimiters (CPatNumeral (loc,n)) key with No_match -> try if !Options.raw_print or !print_no_symbol then raise No_match; extern_symbol_pattern scopes vars pat (Symbols.uninterp_cases_pattern_notations pat) with No_match -> match pat with | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,v7_to_v8_id id))) | PatVar (loc,Anonymous) -> CPatAtom (loc, None) | PatCstr(loc,cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = CPatCstr (loc,extern_reference loc vars (ConstructRef cstrsp),args) in (match na with | Name id -> CPatAlias (loc,p,v7_to_v8_id id) | Anonymous -> p) and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as rule)::rules -> try (* Check the number of arguments expected by the notation *) let loc = match t,n with | PatCstr (_,f,l,_), Some n when List.length l > n -> raise No_match | PatCstr (loc,_,_,_),_ -> loc | PatVar (loc,_),_ -> loc in (* Try matching ... *) let subst = match_aconstr_cases_pattern t pat in (* Try availability of interpretation ... *) match keyrule with | NotationRule (sc,ntn) -> let scopes' = make_current_scopes (tmp_scope, scopes) in (match Symbols.availability_of_notation (sc,ntn) scopes' with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> let scopes = make_current_scopes (scopt, scopes) in let l = List.map (fun (c,(scopt,scl)) -> extern_cases_pattern_in_scope (scopt,List.fold_right push_scope scl scopes) vars c) subst in insert_pat_delimiters (make_pat_notation loc ntn l) key) | SynDefRule kn -> let qid = shortest_qualid_of_syndef vars kn in CPatAtom (loc,Some (Qualid (loc, qid))) with No_match -> extern_symbol_pattern allscopes vars t rules (**********************************************************************) (* Externalising applications *) let occur_name na aty = match na with | Name id -> occur_var_constr_expr id aty | Anonymous -> false let is_projection nargs = function | Some r when not !Options.raw_print & !print_projections -> (try let n = Recordops.find_projection_nparams r + 1 in if n <= nargs then Some n else None with Not_found -> None) | _ -> None let is_nil = function | [CRef ref] -> snd (repr_qualid (snd (qualid_of_reference ref))) = id_of_string "nil" | _ -> false let stdlib_but_length args = function | Some r -> let dir,id = repr_path (sp_of_global r) in (is_coq_root (Lib.library_dp()) or is_coq_root dir) && not (List.mem (string_of_id id) ["Zlength";"length"] && is_nil args) && not (List.mem (string_of_id id) ["In"] && List.length args >= 2 && is_nil (List.tl args)) | None -> false let explicit_code imp q = dummy_loc, if !Options.v7 & not (Options.do_translate()) then ExplByPos q else ExplByName (name_of_implicit imp) let is_hole = function CHole _ -> true | _ -> false let is_significant_implicit a impl tail = not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl)) (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) let explicitize loc inctx impl (cf,f) args = let n = List.length args in let rec exprec q = function | a::args, imp::impl when is_status_implicit imp -> let tail = exprec (q+1) (args,impl) in let visible = !Options.raw_print or (!print_implicits & !print_implicits_explicit_args) or (is_significant_implicit a impl tail & (not (is_inferable_implicit inctx n imp) or (Options.do_translate() & not (stdlib_but_length args cf)))) in if visible then (a,Some (explicit_code imp q)) :: tail else tail | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) | [], _ -> [] in match is_projection (List.length args) cf with | Some i as ip -> if impl <> [] & is_status_implicit (List.nth impl (i-1)) then let f' = match f with CRef f -> f | _ -> assert false in CAppExpl (loc,(ip,f'),args) else let (args1,args2) = list_chop i args in let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in let args1 = exprec 1 (args1,impl1) in let args2 = exprec (i+1) (args2,impl2) in CApp (loc,(Some (List.length args1),f),args1@args2) | None -> let args = exprec 1 (args,impl) in if args = [] then f else CApp (loc, (None, f), args) let extern_global loc impl f = if impl <> [] & List.for_all is_status_implicit impl then CAppExpl (loc, (None, f), []) else CRef f let extern_app loc inctx impl (cf,f) args = if args = [] (* maybe caused by a hidden coercion *) then extern_global loc impl f else if ((!Options.raw_print or (!print_implicits & not !print_implicits_explicit_args)) & List.exists is_status_implicit impl) then CAppExpl (loc, (is_projection (List.length args) cf, f), args) else explicitize loc inctx impl (cf,CRef f) args let rec extern_args extern scopes env args subscopes = match args with | [] -> [] | a::args -> let argscopes, subscopes = match subscopes with | [] -> (None,scopes), [] | scopt::subscopes -> (scopt,scopes), subscopes in extern argscopes env a :: extern_args extern scopes env args subscopes let rec remove_coercions inctx = function | RApp (loc,RRef (_,r),args) as c when inctx & not (!Options.raw_print or !print_coercions or Options.do_translate ()) -> (try match Classops.hide_coercion r with | Some n when n < List.length args -> (* We skip a coercion *) let l = list_skipn n args in let (a,l) = match l with a::l -> (a,l) | [] -> assert false in let (a,l) = (* Recursively remove the head coercions *) match remove_coercions inctx a with | RApp (_,a,l') -> a,l'@l | a -> a,l in if l = [] then a else (* Recursively remove coercions in arguments *) RApp (loc,a,List.map (remove_coercions true) l) | _ -> c with Not_found -> c) | c -> c let rec rename_rawconstr_var id0 id1 = function RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1) | RVar(loc,id) when id=id0 -> RVar(loc,id1) | c -> map_rawconstr (rename_rawconstr_var id0 id1) c let rec share_fix_binders n rbl ty def = match ty,def with RProd(_,na0,t0,b), RLambda(_,na1,t1,m) -> if not(same_rawconstr t0 t1) then List.rev rbl, ty, def else let (na,b,m) = match na0, na1 with Name id0, Name id1 -> if id0=id1 then (na0,b,m) else if not (occur_rawconstr id1 b) then (na1,rename_rawconstr_var id0 id1 b,m) else if not (occur_rawconstr id0 m) then (na1,b,rename_rawconstr_var id1 id0 m) else (* vraiment pas de chance! *) failwith "share_fix_binders: capture" | Name id, Anonymous -> if not (occur_rawconstr id m) then (na0,b,m) else failwith "share_fix_binders: capture" | Anonymous, Name id -> if not (occur_rawconstr id b) then (na1,b,m) else failwith "share_fix_binders: capture" | _ -> (na1,b,m) in share_fix_binders (n-1) ((na,None,t0)::rbl) b m | _ -> List.rev rbl, ty, def (**********************************************************************) (* mapping rawterms to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) let extern_possible_numeral scopes r = try let (sc,n) = uninterp_numeral r in match Symbols.availability_of_numeral sc (make_current_scopes scopes) with | None -> None | Some key -> Some (insert_delimiters (CNumeral(loc_of_rawconstr r,n)) key) with No_match -> None let extern_optimal_numeral scopes r r' = let c = extern_possible_numeral scopes r in let c' = if r==r' then None else extern_possible_numeral scopes r' in match c,c' with | Some n, (Some (CDelimiters _) | None) | _, Some n -> n | _ -> raise No_match (**********************************************************************) (* mapping rawterms to constr_expr *) let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Options.raw_print or !print_no_symbol then raise No_match; extern_optimal_numeral scopes r r' with No_match -> try if !Options.raw_print or !print_no_symbol then raise No_match; extern_symbol scopes vars r' (Symbols.uninterp_notations r') with No_match -> match r' with | RRef (loc,ref) -> extern_global loc (implicits_of_global_out ref) (extern_reference loc vars ref) | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id)) | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n) | RApp (loc,f,args) -> (match f with | RRef (rloc,ref) -> let subscopes = Symbols.find_arguments_scope ref in let args = extern_args (extern true) (snd scopes) vars args subscopes in extern_app loc inctx (implicits_of_global_out ref) (Some ref,extern_reference rloc vars ref) args | RVar (rloc,id) -> (* useful for translation of inductive *) let args = List.map (sub_extern true scopes vars) args in extern_app loc inctx (get_temporary_implicits_out id) (None,Ident (rloc,v7_to_v8_id id)) args | _ -> explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (sub_extern true scopes vars) args)) | RProd (loc,Anonymous,t,c) -> (* Anonymous product are never factorized *) CArrow (loc,extern_type scopes vars t, extern_type scopes vars c) | RLetIn (loc,na,t,c) -> let na = name_app translate_ident na in CLetIn (loc,(loc,na),sub_extern false scopes vars t, extern inctx scopes (add_vname vars na) c) | RProd (loc,na,t,c) -> let t = extern_type scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_prod scopes (add_vname vars na) t c in CProdN (loc,[(dummy_loc,na)::idl,t],c) | RLambda (loc,na,t,c) -> let t = extern_type scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,t],c) | RCases (loc,(typopt,rtntypopt),tml,eqns) -> let pred = option_app (extern_type scopes vars) typopt in let vars' = List.fold_right (name_fold Idset.add) (cases_predicate_names tml) vars in let rtntypopt' = option_app (extern_type scopes vars') !rtntypopt in let tml = List.map (fun (tm,{contents=(na,x)}) -> let na' = match na,tm with Anonymous, RVar (_,id) when !rtntypopt<>None & occur_rawconstr id (out_some !rtntypopt) -> Some Anonymous | Anonymous, _ -> None | Name id, RVar (_,id') when id=id' -> None | Name _, _ -> Some na in (sub_extern false scopes vars tm, (na',option_app (fun (loc,ind,nal) -> let args = List.map (function | Anonymous -> RHole (dummy_loc,InternalHole) | Name id -> RVar (dummy_loc,id)) nal in let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in (extern_type scopes vars t)) x))) tml in let eqns = List.map (extern_eqn (typopt<>None) scopes vars) eqns in CCases (loc,(pred,rtntypopt'),tml,eqns) | ROrderedCase (loc,cs,typopt,tm,bv,{contents = Some x}) -> extern false scopes vars x | ROrderedCase (loc,IfStyle,typopt,tm,bv,_) when Options.do_translate () -> let rec strip_branches = function | (RLambda (_,_,_,c1), RLambda (_,_,_,c2)) -> strip_branches (c1,c2) | x -> x in let c1,c2 = strip_branches (bv.(0),bv.(1)) in msgerrnl (str "Warning: unable to ensure the correctness of the translation of an if-then-else"); let bv = Array.map (sub_extern (typopt<>None) scopes vars) [|c1;c2|] in COrderedCase (loc,IfStyle,option_app (extern_type scopes vars) typopt, sub_extern false scopes vars tm,Array.to_list bv) (* We failed type-checking If and to translate it to CIf *) (* try to remove the dependances in branches anyway *) | ROrderedCase (loc,cs,typopt,tm,bv,_) -> let bv = Array.map (sub_extern (typopt<>None) scopes vars) bv in COrderedCase (loc,cs,option_app (extern_type scopes vars) typopt, sub_extern false scopes vars tm,Array.to_list bv) | RLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,nal, (option_app (fun _ -> na) typopt, option_app (extern_type scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern false scopes (List.fold_left add_vname vars nal) b) | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, (option_app (fun _ -> na) typopt, option_app (extern_type scopes (add_vname vars na)) typopt), sub_extern false scopes vars b1, sub_extern false scopes vars b2) | RRec (loc,fk,idv,blv,tyv,bv) -> let vars' = Array.fold_right Idset.add idv vars in (match fk with | RFix (nv,n) -> let listdecl = Array.mapi (fun i fi -> let (bl,ty,def) = if Options.do_translate() then let n = List.fold_left (fun n (_,obd,_) -> if obd=None then n-1 else n) nv.(i) blv.(i) in share_fix_binders n (List.rev blv.(i)) tyv.(i) bv.(i) else blv.(i), tyv.(i), bv.(i) in let (ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in (fi,nv.(i), bl, extern_type scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) | RCoFix n -> let listdecl = Array.mapi (fun i fi -> let (ids,bl) = extern_local_binder scopes vars blv.(i) in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in (fi,bl,extern_type scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) | RSort (loc,s) -> let s = match s with | RProp _ -> s | RType (Some _) when !print_universes -> s | RType _ -> RType None in CSort (loc,s) | RHole (loc,e) -> CHole loc | RCast (loc,c,t) -> CCast (loc,sub_extern true scopes vars c,extern_type scopes vars t) | RDynamic (loc,d) -> CDynamic (loc,d) and extern_type (_,scopes) = extern true (Some Symbols.type_scope,scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars aty = function | RProd (loc,(Name id as na),ty,c) when same aty (extern_type scopes vars (anonymize_if_reserved na ty)) & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) -> let id = translate_ident id in let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in ((loc,Name id)::nal,c) | c -> ([],extern_type scopes vars c) and factorize_lambda inctx scopes vars aty = function | RLambda (loc,na,ty,c) when same aty (extern_type scopes vars (anonymize_if_reserved na ty)) & not (occur_name na aty) (* To avoid na in ty' escapes scope *) -> let na = name_app translate_ident na in let (nal,c) = factorize_lambda inctx scopes (add_vname vars na) aty c in ((loc,na)::nal,c) | c -> ([],sub_extern inctx scopes vars c) and extern_local_binder scopes vars = function [] -> ([],[]) | (na,Some bd,ty)::l -> let na = name_app translate_ident na in let (ids,l) = extern_local_binder scopes (name_fold Idset.add na vars) l in (na::ids, LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l) | (na,None,ty)::l -> let na = name_app translate_ident na in let ty = extern_type scopes vars (anonymize_if_reserved na ty) in (match extern_local_binder scopes (name_fold Idset.add na vars) l with (ids,LocalRawAssum(nal,ty')::l) when same ty ty' & match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::ids, LocalRawAssum((dummy_loc,na)::nal,ty')::l) | (ids,l) -> (na::ids, LocalRawAssum([(dummy_loc,na)],ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, extern inctx scopes vars c) and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as rule)::rules -> let loc = Rawterm.loc_of_rawconstr t in try (* Adjusts to the number of arguments expected by the notation *) let (t,args) = match t,n with | RApp (_,f,args), Some n when List.length args > n -> let args1, args2 = list_chop n args in RApp (dummy_loc,f,args1), args2 | _ -> t,[] in (* Try matching ... *) let subst = match_aconstr t pat in (* Try availability of interpretation ... *) let e = match keyrule with | NotationRule (sc,ntn) -> let scopes' = make_current_scopes (tmp_scope, scopes) in (match Symbols.availability_of_notation (sc,ntn) scopes' with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> let scopes = make_current_scopes (scopt, scopes) in let l = List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true (scopt,List.fold_right push_scope scl scopes) vars c) subst in insert_delimiters (make_notation loc ntn l) key) | SynDefRule kn -> CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in if args = [] then e else (* TODO: compute scopt for the extra args, in case, head is a ref *) explicitize loc false [] (None,e) (List.map (extern true allscopes vars) args) with No_match -> extern_symbol allscopes vars t rules let extern_rawconstr vars c = extern false (None,Symbols.current_scopes()) vars c let extern_rawtype vars c = extern_type (None,Symbols.current_scopes()) vars c let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,Symbols.current_scopes()) vars p (******************************************************************) (* Main translation function from constr -> constr_expr *) let loc = dummy_loc (* for constr and pattern, locations are lost *) let extern_constr_gen at_top scopt env t = let vars = vars_of_env env in let avoid = if at_top then ids_of_context env else [] in extern (not at_top) (scopt,Symbols.current_scopes()) vars (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t) let extern_constr_in_scope at_top scope env t = extern_constr_gen at_top (Some scope) env t let extern_constr at_top env t = extern_constr_gen at_top None env t (******************************************************************) (* Main translation function from pattern -> constr_expr *) let rec raw_of_pat tenv env = function | PRef ref -> RRef (loc,ref) | PVar id -> RVar (loc,id) | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat tenv env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id | Anonymous -> anomaly "rawconstr_of_pattern: index to an anonymous variable" with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in RVar (loc,id) | PMeta None -> RHole (loc,InternalHole) | PMeta (Some n) -> RPatVar (loc,(false,n)) | PApp (f,args) -> RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args) | PSoApp (n,args) -> RApp (loc,RPatVar (loc,(true,n)), List.map (raw_of_pat tenv env) args) | PProd (na,t,c) -> RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c) | PLetIn (na,t,c) -> RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) | PLambda (na,t,c) -> RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) | PCase ((_,(IfStyle|LetStyle as cs)),typopt,tm,bv) -> ROrderedCase (loc,cs,option_app (raw_of_pat tenv env) typopt, raw_of_pat tenv env tm,Array.map (raw_of_pat tenv env) bv, ref None) | PCase ((_,cs),typopt,tm,[||]) -> RCases (loc,(option_app (raw_of_pat tenv env) typopt,ref None (* TODO *)), [raw_of_pat tenv env tm,ref (Anonymous,None)],[]) | PCase ((Some ind,cs),typopt,tm,bv) -> let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env) (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) tenv avoid ind cs typopt k tm bv | PCase _ -> error "Unsupported case-analysis while printing pattern" | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f) | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c) | PSort s -> RSort (loc,s) and raw_of_eqn tenv env constr construct_nargs branch = let make_pat x env b ids = let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in let id = next_name_away_with_default "x" x avoid in PatVar (dummy_loc,Name id),(Name id)::env,id::ids in let rec buildrec ids patlist env n b = if n=0 then (dummy_loc, ids, [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], raw_of_pat tenv env b) else match b with | PLambda (x,_,b) -> let pat,new_env,new_ids = make_pat x env b ids in buildrec new_ids (pat::patlist) new_env (n-1) b | PLetIn (x,_,b) -> let pat,new_env,new_ids = make_pat x env b ids in buildrec new_ids (pat::patlist) new_env (n-1) b | _ -> error "Unsupported branch in case-analysis while printing pattern" in buildrec [] [] env construct_nargs branch let extern_pattern tenv env pat = extern true (None,Symbols.current_scopes()) Idset.empty (raw_of_pat tenv env pat)