diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 1235 |
1 files changed, 157 insertions, 1078 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 25167865..6442cb94 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml,v 1.85.2.7 2006/01/05 12:00:35 herbelin Exp $ *) +(* $Id: constrextern.ml 8675 2006-03-31 18:21:20Z herbelin $ *) (*i*) open Pp @@ -25,7 +25,7 @@ open Topconstr open Rawterm open Pattern open Nametab -open Symbols +open Notation open Reserve (*i*) @@ -54,7 +54,7 @@ let print_coercions = ref false (* This forces printing universe names of Type{.} *) let print_universes = ref false -(* This suppresses printing of numeral and symbols *) +(* This suppresses printing of primitive tokens (e.g. numeral) and symbols *) let print_no_symbol = ref false (* This governs printing of projections using the dot notation symbols *) @@ -69,13 +69,6 @@ let with_universes f = Options.with_option print_universes f let without_symbols f = Options.with_option print_no_symbol f let with_meta_as_hole f = Options.with_option print_meta_as_hole f -(* For the translator *) -let temporary_implicits_out = ref [] -let set_temporary_implicits_out l = temporary_implicits_out := l -let get_temporary_implicits_out id = - try List.assoc id !temporary_implicits_out - with Not_found -> [] - (**********************************************************************) (* Various externalisation functions *) @@ -83,9 +76,13 @@ 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) +let insert_pat_delimiters loc p = function + | None -> p + | Some sc -> CPatDelimiters (loc,sc,p) + +let insert_pat_alias loc p = function + | Anonymous -> p + | Name id -> CPatAlias (loc,p,id) (**********************************************************************) (* conversion of references *) @@ -96,8 +93,7 @@ let ids_of_ctxt ctxt = (function c -> match kind_of_term c with | Var id -> id | _ -> - error - "Termast: arbitrary substitution of references not yet implemented") + error "arbitrary substitution of references not implemented") ctxt) let idopt_of_name = function @@ -114,7 +110,7 @@ let extern_evar loc n = let raw_string_of_ref = function | ConstRef kn -> - "CONST("^(string_of_kn kn)^")" + "CONST("^(string_of_con kn)^")" | IndRef (kn,i) -> "IND("^(string_of_kn kn)^","^(string_of_int i)^")" | ConstructRef ((kn,i),j) -> @@ -123,863 +119,8 @@ let raw_string_of_ref = function | 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<r2 et non 0<r1 ce - qui est plus général mais différent de Rmult_le_compat ? *) -"Rmult_lt", ([],"Rmult_gt_0_lt_compat"); (* Hybride aussi *) -"Rmult_lt_0", ([],"Rmult_ge_0_gt_0_lt_compat"); (* Un truc hybride *) -(* - "Rlt_minus" -> - "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) + try Qualid (loc,shortest_qualid_of_global vars r) with Not_found -> (* happens in debugger *) Ident (loc,id_of_string (raw_string_of_ref r)) @@ -994,7 +135,7 @@ let rec check_same_pattern p1 p2 = | 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 -> () + | CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> () | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 -> check_same_pattern e1 e2 | _ -> failwith "not same pattern" @@ -1046,18 +187,15 @@ let rec check_same_type ty1 ty2 = 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) -> + | 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 -> () + | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> () | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 -> check_same_type e1 e2 | _ when ty1=ty2 -> () @@ -1118,7 +256,7 @@ let rec same_raw c d = 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)}) -> + (fun (t1,(al1,oind1)) (t2,(al2,oind2)) -> same_raw t1 t2; if al1 <> al2 then failwith "RCases"; option_iter2(fun (_,i1,nl1) (_,i2,nl2) -> @@ -1126,9 +264,6 @@ let rec same_raw c d = 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; @@ -1147,8 +282,8 @@ let rec same_raw c d = | 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 + | 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" @@ -1174,7 +309,7 @@ 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 expand_curly_brackets loc mknot ntn l = let ntn' = ref ntn in let rec expand_ntn i = function @@ -1187,58 +322,45 @@ let expand_curly_brackets make_ntn ntn l = ntn' := String.sub !ntn' 0 p ^ "_" ^ String.sub !ntn' (p+5) (String.length !ntn' -p-5); - make_ntn "{ _ }" [a] end + mknot (loc,"{ _ }",[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 + mknot (loc,!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 destPrim = function CPrim(_,t) -> Some t | _ -> None +let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None -let make_pat_notation loc ntn l = +let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn - then expand_curly_brackets (fun n l -> CPatNotation (loc,n,l)) ntn l - else match ntn,l with + then expand_curly_brackets loc mknot ntn l + else match ntn,List.map destprim 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) + | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p -> + mknot (loc,ntn,[mknot (loc,"( _ )",l)]) + | _ -> + match decompose_notation_key ntn, l with + | [Terminal "-"; Terminal x], [] -> + (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x))) + with _ -> mknot (loc,ntn,[])) + | [Terminal x], [] -> + (try mkprim (loc, Numeral (Bigint.of_string x)) + with _ -> mknot (loc,ntn,[])) + | _ -> + mknot (loc,ntn,l) +let make_notation loc ntn l = + make_notation_gen loc ntn + (fun (loc,ntn,l) -> CNotation (loc,ntn,l)) + (fun (loc,p) -> CPrim (loc,p)) + destPrim 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 make_pat_notation loc ntn l = + make_notation_gen loc ntn + (fun (loc,ntn,l) -> CPatNotation (loc,ntn,l)) + (fun (loc,p) -> CPatPrim (loc,p)) + destPatPrim l let bind_env sigma var v = try @@ -1251,10 +373,10 @@ let bind_env sigma var v = 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 + | a, AHole _ -> sigma | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ -> let nparams = - (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in + (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let l2 = match a2 with | ARef (ConstructRef r2) when r1 = r2 -> [] @@ -1281,32 +403,30 @@ let match_aconstr_cases_pattern c (metas_scl,pat) = 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 + let (na,sc,p) = uninterp_prim_token_cases_pattern pat in + match availability_of_prim_token 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 + let loc = pattern_loc pat in + insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na 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) + (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,Name id) -> CPatAtom (loc,Some (Ident (loc,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) + insert_pat_alias loc p na and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match - | (keyrule,pat,n as rule)::rules -> + | (keyrule,pat,n as _rule)::rules -> try (* Check the number of arguments expected by the notation *) let loc = match t,n with @@ -1320,7 +440,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function match keyrule with | NotationRule (sc,ntn) -> let scopes' = make_current_scopes (tmp_scope, scopes) in - (match Symbols.availability_of_notation (sc,ntn) scopes' with + (match availability_of_notation (sc,ntn) scopes' with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) @@ -1331,13 +451,16 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function 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) + insert_pat_delimiters loc (make_pat_notation loc ntn l) key) | SynDefRule kn -> let qid = shortest_qualid_of_syndef vars kn in - CPatAtom (loc,Some (Qualid (loc, qid))) + CPatAtom (loc,Some (Qualid (loc, qid))) with No_match -> extern_symbol_pattern allscopes vars t rules +let extern_cases_pattern vars p = + extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p + (**********************************************************************) (* Externalising applications *) @@ -1354,24 +477,6 @@ let is_projection nargs = function 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 = @@ -1388,10 +493,12 @@ let explicitize loc inctx impl (cf,f) args = !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)))) + (not (is_inferable_implicit inctx n imp))) in - if visible then (a,Some (explicit_code imp q)) :: tail else tail + if visible then + (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: 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 @@ -1440,9 +547,7 @@ let rec 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 ()) + when inctx & not (!Options.raw_print or !print_coercions) -> (try match Classops.hide_coercion r with | Some n when n < List.length args -> @@ -1498,18 +603,18 @@ let rec share_fix_binders n 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 = +let extern_possible_prim_token scopes r = try - let (sc,n) = uninterp_numeral r in - match Symbols.availability_of_numeral sc (make_current_scopes scopes) with + let (sc,n) = uninterp_prim_token r in + match availability_of_prim_token sc (make_current_scopes scopes) with | None -> None - | Some key -> Some (insert_delimiters (CNumeral(loc_of_rawconstr r,n)) key) + | Some key -> Some (insert_delimiters (CPrim (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 +let extern_optimal_prim_token scopes r r' = + let c = extern_possible_prim_token scopes r in + let c' = if r==r' then None else extern_possible_prim_token scopes r' in match c,c' with | Some n, (Some (CDelimiters _) | None) | _, Some n -> n | _ -> raise No_match @@ -1521,17 +626,19 @@ 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' + extern_optimal_prim_token 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') + extern_symbol scopes vars r' (uninterp_notations r') with No_match -> match r' with | RRef (loc,ref) -> - extern_global loc (implicits_of_global_out ref) + extern_global loc (implicits_of_global ref) (extern_reference loc vars ref) - | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id)) + | RVar (loc,id) -> CRef (Ident (loc,id)) + + | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n @@ -1540,50 +647,43 @@ let rec extern inctx scopes vars r = | RApp (loc,f,args) -> (match f with | RRef (rloc,ref) -> - let subscopes = Symbols.find_arguments_scope ref in + let subscopes = 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) + extern_app loc inctx (implicits_of_global 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) + CArrow (loc,extern_typ scopes vars t, extern_typ 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 t = extern_typ 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 t = extern_typ 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 + | RCases (loc,rtntypopt,tml,eqns) -> 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 rtntypopt' = option_app (extern_typ scopes vars') rtntypopt in + let tml = List.map (fun (tm,(na,x)) -> let na' = match na,tm with Anonymous, RVar (_,id) when - !rtntypopt<>None & occur_rawconstr id (out_some !rtntypopt) + rtntypopt<>None & occur_rawconstr id (out_some rtntypopt) -> Some Anonymous | Anonymous, _ -> None | Name id, RVar (_,id') when id=id' -> None @@ -1591,47 +691,24 @@ let rec extern inctx scopes vars r = (sub_extern false scopes vars tm, (na',option_app (fun (loc,ind,nal) -> let args = List.map (function - | Anonymous -> RHole (dummy_loc,InternalHole) + | Anonymous -> RHole (dummy_loc,Evd.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) + (extern_typ scopes vars t)) x))) tml in + let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in + CCases (loc,rtntypopt',tml,eqns) | 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), + option_app (extern_typ 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), + option_app (extern_typ 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) -> @@ -1640,17 +717,12 @@ let rec extern inctx scopes vars r = | 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 (bl,ty,def) = 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, + let n, ro = fst nv.(i), extern_recursion_order scopes vars (snd nv.(i)) in + (fi, (n, ro), bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) @@ -1660,7 +732,7 @@ let rec extern inctx scopes vars r = 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), + (fi,bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) @@ -1674,30 +746,28 @@ let rec extern inctx scopes vars r = | RHole (loc,e) -> CHole loc - | RCast (loc,c,t) -> - CCast (loc,sub_extern true scopes vars c,extern_type scopes vars t) + | RCast (loc,c,k,t) -> + CCast (loc,sub_extern true scopes vars c,k,extern_typ scopes vars t) | RDynamic (loc,d) -> CDynamic (loc,d) -and extern_type (_,scopes) = extern true (Some Symbols.type_scope,scopes) +and extern_typ (_,scopes) = extern true (Some Notation.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)) + when same aty (extern_typ 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 + -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in ((loc,Name id)::nal,c) - | c -> ([],extern_type scopes vars c) + | c -> ([],extern_typ 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)) + when same aty (extern_typ 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) = + -> 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) @@ -1705,15 +775,13 @@ and factorize_lambda inctx scopes vars aty = function 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 + let ty = extern_typ 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' & @@ -1731,7 +799,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match - | (keyrule,pat,n as rule)::rules -> + | (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 *) @@ -1747,7 +815,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function match keyrule with | NotationRule (sc,ntn) -> let scopes' = make_current_scopes (tmp_scope, scopes) in - (match Symbols.availability_of_notation (sc,ntn) scopes' with + (match availability_of_notation (sc,ntn) scopes' with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) @@ -1769,14 +837,16 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function with No_match -> extern_symbol allscopes vars t rules -let extern_rawconstr vars c = - extern false (None,Symbols.current_scopes()) vars c +and extern_recursion_order scopes vars = function + RStructRec -> CStructRec + | RWfRec c -> CWfRec (extern true 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 +let extern_rawconstr vars c = + extern false (None,Notation.current_scopes()) vars c + +let extern_rawtype vars c = + extern_typ (None,Notation.current_scopes()) vars c (******************************************************************) (* Main translation function from constr -> constr_expr *) @@ -1784,10 +854,10 @@ let extern_cases_pattern vars p = 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 r = Detyping.detype at_top avoid (names_of_rel_context env) t in + let vars = vars_of_env env in + extern (not at_top) (scopt,Notation.current_scopes()) vars r let extern_constr_in_scope at_top scope env t = extern_constr_gen at_top (Some scope) env t @@ -1795,13 +865,18 @@ let extern_constr_in_scope at_top scope env t = let extern_constr at_top env t = extern_constr_gen at_top None env t +let extern_type at_top env t = + let avoid = if at_top then ids_of_context env else [] in + let r = Detyping.detype at_top avoid (names_of_rel_context env) t in + extern_rawtype (vars_of_env env) r + (******************************************************************) (* Main translation function from pattern -> constr_expr *) -let rec raw_of_pat tenv env = function +let rec raw_of_pat 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)) + | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -1809,37 +884,41 @@ let rec raw_of_pat tenv env = function 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 None -> RHole (loc,Evd.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) + RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args) | PSoApp (n,args) -> RApp (loc,RPatVar (loc,(true,n)), - List.map (raw_of_pat tenv env) args) + List.map (raw_of_pat env) args) | PProd (na,t,c) -> - RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c) + RProd (loc,na,raw_of_pat env t,raw_of_pat (na::env) c) | PLetIn (na,t,c) -> - RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) + RLetIn (loc,na,raw_of_pat env t, raw_of_pat (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) + RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) | 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)],[]) + if typopt <> None then failwith "TODO: PCase to RCases"; + RCases (loc,(*(option_app (raw_of_pat env) typopt,*)None, + [raw_of_pat env tm,(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) + let mib,mip = lookup_mind_specif (Global.env()) ind in + let k = mip.Declarations.mind_nrealargs in + let nparams = mib.Declarations.mind_nparams in + let cstrnargs = mip.Declarations.mind_consnrealdecls in + Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env) (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) - tenv avoid ind cs typopt k tm bv + avoid (ind,cs,nparams,cstrnargs,k) typopt 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) + | PFix f -> Detyping.detype false [] env (mkFix f) + | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) -and raw_of_eqn tenv env constr construct_nargs branch = +and raw_of_eqns env constructs consnargsl bl = + Array.to_list (array_map3 (raw_of_eqn env) constructs consnargsl bl) + +and raw_of_eqn 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 @@ -1849,7 +928,7 @@ and raw_of_eqn tenv env constr construct_nargs branch = if n=0 then (dummy_loc, ids, [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - raw_of_pat tenv env b) + raw_of_pat env b) else match b with | PLambda (x,_,b) -> @@ -1865,6 +944,6 @@ and raw_of_eqn tenv env constr construct_nargs branch = 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) +let extern_constr_pattern env pat = + extern true (None,Notation.current_scopes()) Idset.empty + (raw_of_pat env pat) |