summaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /interp/constrextern.ml
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml1235
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)