summaryrefslogtreecommitdiff
path: root/interp
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
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml1235
-rw-r--r--interp/constrextern.mli14
-rw-r--r--interp/constrintern.ml539
-rw-r--r--interp/constrintern.mli113
-rw-r--r--interp/coqlib.ml195
-rw-r--r--interp/coqlib.mli62
-rw-r--r--interp/genarg.ml49
-rw-r--r--interp/genarg.mli23
-rw-r--r--interp/modintern.ml10
-rw-r--r--interp/modintern.mli2
-rw-r--r--interp/notation.ml (renamed from interp/symbols.ml)354
-rw-r--r--interp/notation.mli (renamed from interp/symbols.mli)70
-rw-r--r--interp/ppextend.ml2
-rw-r--r--interp/ppextend.mli2
-rw-r--r--interp/reserve.ml14
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/syntax_def.ml22
-rw-r--r--interp/syntax_def.mli9
-rw-r--r--interp/topconstr.ml482
-rw-r--r--interp/topconstr.mli51
20 files changed, 1222 insertions, 2028 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)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0dcdffeb..1fc44250 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrextern.mli,v 1.11.2.3 2005/01/21 16:41:50 herbelin Exp $ i*)
+(*i $Id: constrextern.mli 7837 2006-01-11 09:47:32Z herbelin $ i*)
(*i*)
open Util
@@ -20,13 +20,10 @@ open Nametab
open Rawterm
open Pattern
open Topconstr
-open Symbols
+open Notation
(*i*)
(* v7->v8 translation *)
-val id_of_v7_string : string -> identifier
-val v7_to_v8_id : identifier -> identifier (* v7->v8 translation *)
-val shortest_qualid_of_v7_global : Idset.t -> global_reference -> qualid
val check_same_type : constr_expr -> constr_expr -> unit
(* Translation of pattern, cases pattern, rawterm and term into syntax
@@ -35,7 +32,7 @@ val check_same_type : constr_expr -> constr_expr -> unit
val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
val extern_rawtype : Idset.t -> rawconstr -> constr_expr
-val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
+val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
(* If [b=true] in [extern_constr b env c] then the variables in the first
level of quantification clashing with the variables in [env] are renamed *)
@@ -43,6 +40,7 @@ val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
val extern_constr : bool -> env -> constr -> constr_expr
val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
val extern_reference : loc -> Idset.t -> global_reference -> reference
+val extern_type : bool -> env -> types -> constr_expr
(* Printing options *)
val print_implicits : bool ref
@@ -71,7 +69,3 @@ val without_symbols : ('a -> 'b) -> 'a -> 'b
(* This prints metas as anonymous holes *)
val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
-
-(* For v8 translation *)
-val set_temporary_implicits_out :
- (identifier * Impargs.implicits_list) list -> unit
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index bacdb387..6fcd9d7a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml,v 1.58.2.7 2005/11/19 10:34:35 herbelin Exp $ *)
+(* $Id: constrintern.ml 8654 2006-03-22 15:36:58Z msozeau $ *)
open Pp
open Util
@@ -18,9 +18,10 @@ open Impargs
open Rawterm
open Pattern
open Pretyping
+open Cases
open Topconstr
open Nametab
-open Symbols
+open Notation
(* To interpret implicits and arg scopes of recursive variables in
inductive types and recursive definitions *)
@@ -42,10 +43,6 @@ let for_grammar f x =
let variables_bind = ref false
-(* For the translator *)
-let temporary_implicits_in = ref []
-let set_temporary_implicits_in l = temporary_implicits_in := l
-
(**********************************************************************)
(* Internalisation errors *)
@@ -154,10 +151,8 @@ let add_glob loc ref =
i*)
let sp = Nametab.sp_of_global ref in
let id = let _,id = repr_path sp in string_of_id id in
- let dir = Lib.file_part ref in
- if dir <> None then
- let dp = string_of_dirpath (out_some dir) in
- dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id)
+ let dp = string_of_dirpath (Lib.library_part ref) in
+ dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id)
let loc_of_notation f loc args ntn =
if args=[] or ntn.[0] <> '_' then fst (unloc loc)
@@ -166,20 +161,19 @@ let loc_of_notation f loc args ntn =
let ntn_loc = loc_of_notation constr_loc
let patntn_loc = loc_of_notation cases_pattern_loc
-let dump_notation_location =
- fun pos ntn ((path,df),sc) ->
- let rec next growing =
- let loc = Lexer.location_function !token_number in
- let (bp,_) = unloc loc in
- if growing then if bp >= pos then loc else (incr token_number;next true)
- else if bp = pos then loc
- else if bp > pos then (decr token_number;next false)
- else (incr token_number;next true) in
- let loc = next (pos >= !last_pos) in
- last_pos := pos;
- let path = string_of_dirpath path in
- let sc = match sc with Some sc -> " "^sc | None -> "" in
- dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
+let dump_notation_location pos ((path,df),sc) =
+ let rec next growing =
+ let loc = Lexer.location_function !token_number in
+ let (bp,_) = unloc loc in
+ if growing then if bp >= pos then loc else (incr token_number;next true)
+ else if bp = pos then loc
+ else if bp > pos then (decr token_number;next false)
+ else (incr token_number;next true) in
+ let loc = next (pos >= !last_pos) in
+ last_pos := pos;
+ let path = string_of_dirpath path in
+ let sc = match sc with Some sc -> " "^sc | None -> "" in
+ dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
(**********************************************************************)
(* Contracting "{ _ }" in notations *)
@@ -249,15 +243,14 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
[vars2] is the set of global variables, env is the set of variables
abstracted until this point *)
-let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
+let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
let (vars1,unbndltacvars) = ltacvars in
(* Is [id] an inductive type potentially with implicit *)
try
let l,impl,argsc = List.assoc id impls in
let l = List.map
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
- RVar (loc,id), impl, argsc,
- (if !Options.v7 & !interning_grammar then [] else l)
+ RVar (loc,id), impl, argsc, l
with Not_found ->
(* Is [id] bound in current env or is an ltac var bound to constr *)
if Idset.mem id env or List.mem id vars1
@@ -273,7 +266,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
try
match List.assoc id unbndltacvars with
| None -> user_err_loc (loc,"intern_var",
- pr_id id ++ str " ist not bound to a term")
+ str "variable " ++ pr_id id ++ str " should be bound to a term")
| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
with Not_found ->
(* Is [id] a goal or section variable *)
@@ -287,7 +280,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
(* [id] a goal variable *)
RVar (loc,id), [], [], []
-let find_appl_head_data (_,_,_,_,impls) = function
+let find_appl_head_data (_,_,_,(_,impls)) = function
| RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
| x -> x,[],[],[]
@@ -320,13 +313,6 @@ let intern_reference env lvar = function
| Qualid (loc, qid) ->
find_appl_head_data lvar (intern_qualid loc qid)
| Ident (loc, id) ->
- (* For old ast syntax compatibility *)
- if (string_of_id id).[0] = '$' then RVar (loc,id),[],[],[] else
- (* End old ast syntax compatibility *)
- (* Pour traduction des implicites d'inductifs et points-fixes *)
- try RVar (loc,id), List.assoc id !temporary_implicits_in, [], []
- with Not_found ->
- (* Fin pour traduction *)
try intern_var env lvar loc id
with Not_found ->
try find_appl_head_data lvar (intern_qualid loc (make_short_qualid id))
@@ -336,10 +322,10 @@ let intern_reference env lvar = function
else raise e
let interp_reference vars r =
- let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r
+ let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r
in r
-let apply_scope_env (ids,_,scopes as env) = function
+let apply_scope_env (ids,_,scopes) = function
| [] -> (ids,None,scopes), []
| sc::scl -> (ids,sc,scopes), scl
@@ -357,6 +343,21 @@ let rec simple_adjust_scopes = function
(**********************************************************************)
(* Cases *)
+let product_of_cases_patterns ids idspl =
+ List.fold_right (fun (ids,pl) (ids',ptaill) ->
+ (ids@ids',
+ (* Cartesian prod of the or-pats for the nth arg and the tail args *)
+ List.flatten (
+ List.map (fun (subst,p) ->
+ List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)))
+ idspl (ids,[[],[]])
+
+let simple_product_of_cases_patterns pl =
+ List.fold_right (fun pl ptaill ->
+ List.flatten (List.map (fun (subst,p) ->
+ List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl))
+ pl [[],[]]
+
(* Check linearity of pattern-matching *)
let rec has_duplicate = function
| [] -> None
@@ -372,32 +373,33 @@ let check_linearity lhs ids =
| None ->
()
-(* Warns if some pattern variable starts with uppercase *)
-let check_uppercase loc ids =
-(* A quoi ça sert ? Pour l'extraction vers ML ? Maintenant elle est externe
- let is_uppercase_var v =
- match (string_of_id v).[0] with 'A'..'Z' -> true | _ -> false
- in
- let warning_uppercase loc uplid =
- let vars = h 0 (prlist_with_sep pr_coma pr_id uplid) in
- let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in
- warn (str ("the variable"^s1) ++ vars ++
- str (" start"^s2^"with an upper case letter in pattern")) in
- let uplid = List.filter is_uppercase_var ids in
- if uplid <> [] then warning_uppercase loc uplid
-*)
- ()
-
(* Match the number of pattern against the number of matched args *)
let check_number_of_pattern loc n l =
let p = List.length l in
if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p)))
+let check_or_pat_variables loc ids idsl =
+ if List.exists ((<>) ids) idsl then
+ user_err_loc (loc, "", str
+ "The components of this disjunctive pattern must bind the same variables")
+
+let check_constructor_length env loc cstr pl pl0 =
+ let n = List.length pl + List.length pl0 in
+ let nargs = Inductiveops.constructor_nrealargs env cstr in
+ let nhyps = Inductiveops.constructor_nrealhyps env cstr in
+ if n <> nargs && n <> nhyps (* i.e. with let's *) then
+ error_wrong_numarg_constructor_loc loc env cstr nargs
+
+let check_inductive_length env (loc,ind,nal) =
+ let n = Inductiveops.inductive_nargs env ind in
+ if n <> List.length nal then
+ error_wrong_numarg_inductive_loc loc env ind n
+
(* Manage multiple aliases *)
(* [merge_aliases] returns the sets of all aliases encountered at this
point and a substitution mapping extra aliases to the first one *)
-let merge_aliases (ids,subst as aliases) id =
+let merge_aliases (ids,subst as _aliases) id =
ids@[id], if ids=[] then subst else (id, List.hd ids)::subst
let alias_of = function
@@ -414,13 +416,15 @@ let decode_patlist_value = function
| CPatCstr (_,_,l) -> l
| _ -> anomaly "Ill-formed list argument of notation"
-let rec subst_pat_iterator y t = function
+let rec subst_pat_iterator y t (subst,p) = match p with
| PatVar (_,id) as x ->
- if id = Name y then t else x
+ if id = Name y then t else [subst,x]
| PatCstr (loc,id,l,alias) ->
- PatCstr (loc,id,List.map (subst_pat_iterator y t) l,alias)
+ let l' = List.map (fun a -> (subst_pat_iterator y t ([],a))) l in
+ let pl = simple_product_of_cases_patterns l' in
+ List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
-let subst_cases_pattern loc aliases intern subst scopes a =
+let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a =
let rec aux aliases subst = function
| AVar id ->
begin
@@ -430,7 +434,7 @@ let subst_cases_pattern loc aliases intern subst scopes a =
let (a,(scopt,subscopes)) = List.assoc id subst in
intern (subscopes@scopes) ([],[]) scopt a
with Not_found ->
- if id = ldots_var then [[],[]], PatVar (loc,Name id) else
+ if id = ldots_var then [],[[], PatVar (loc,Name id)] else
anomaly ("Unbound pattern notation variable: "^(string_of_id id))
(*
(* Happens for local notation joint with inductive/fixpoint defs *)
@@ -440,24 +444,28 @@ let subst_cases_pattern loc aliases intern subst scopes a =
*)
end
| ARef (ConstructRef c) ->
- [aliases], PatCstr (loc,c, [], alias_of aliases)
+ (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)])
| AApp (ARef (ConstructRef (ind,_ as c)),args) ->
- let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+ let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
let _,args = list_chop nparams args in
- let (idsl,pl) = List.split (List.map (aux ([],[]) subst) args) in
- aliases::List.flatten idsl, PatCstr (loc,c,pl,alias_of aliases)
+ let idslpll = List.map (aux ([],[]) subst) args in
+ let ids',pll = product_of_cases_patterns ids idslpll in
+ let pl' = List.map (fun (subst,pl) ->
+ subst,PatCstr (loc,c,pl,alias_of aliases)) pll in
+ ids', pl'
| AList (x,_,iter,terminator,lassoc) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (a,(scopt,subscopes)) = List.assoc x subst in
- let idslt,termin = aux ([],[]) subst terminator in
+ let termin = aux ([],[]) subst terminator in
let l = decode_patlist_value a in
let idsl,v =
- List.fold_right (fun a (allidsl,t) ->
- let idsl,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in
- idsl::allidsl, subst_pat_iterator ldots_var t u)
- (if lassoc then List.rev l else l) ([idslt],termin) in
- aliases::List.flatten idsl, v
+ List.fold_right (fun a (tids,t) ->
+ let uids,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in
+ let pll = List.map (subst_pat_iterator ldots_var t) u in
+ tids@uids, List.flatten pll)
+ (if lassoc then List.rev l else l) termin in
+ ids@idsl, v
with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t -> user_err_loc (loc,"",str "Invalid notation for pattern")
@@ -476,7 +484,7 @@ let rec patt_of_rawterm loc cstr =
| RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2))
| RApp (_,RRef(_,(ConstructRef c as x)),pl) ->
if !dump then add_glob loc x;
- let (_,mib) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
+ let (mib,_) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
let npar = mib.Declarations.mind_nparams in
let (params,args) =
if List.length pl <= npar then (pl,[]) else
@@ -506,7 +514,7 @@ let find_constructor ref =
let rec unf = function
| ConstRef cst ->
let v = Environ.constant_value (Global.env()) cst in
- unf (reference_of_constr v)
+ unf (global_of_constr v)
| ConstructRef c ->
if !dump then add_glob loc r;
c, []
@@ -524,7 +532,7 @@ let maybe_constructor ref =
| InternalisationError _ -> VarPat (find_pattern_variable ref)
(* patt var also exists globally but does not satisfy preconditions *)
| (Environ.NotEvaluableConst _ | Not_found) ->
- warn (str "pattern " ++ pr_reference ref ++
+ if_verbose msg_warning (str "pattern " ++ pr_reference ref ++
str " is understood as a pattern variable");
VarPat (find_pattern_variable ref)
@@ -533,48 +541,63 @@ let mustbe_constructor loc ref =
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalisationError (loc,NotAConstructor ref))
-let rec intern_cases_pattern scopes aliases tmp_scope = function
+let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
+ function
| CPatAlias (loc, p, id) ->
let aliases' = merge_aliases aliases id in
- intern_cases_pattern scopes aliases' tmp_scope p
+ intern_cases_pattern genv scopes aliases' tmp_scope p
| CPatCstr (loc, head, pl) ->
let c,pl0 = mustbe_constructor loc head in
let argscs =
simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
- let (idsl,pl') =
- List.split (List.map2 (intern_cases_pattern scopes ([],[])) argscs pl)
- in
- (aliases::(List.flatten idsl), PatCstr (loc,c,pl0@pl',alias_of aliases))
- | CPatNotation (loc,"- _",[CPatNumeral(_,Bignat.POS p)]) ->
- let scopes = option_cons tmp_scope scopes in
- ([aliases],
- Symbols.interp_numeral_as_pattern loc (Bignat.NEG p)
- (alias_of aliases) scopes)
+ check_constructor_length genv loc c pl0 pl;
+ let idslpl =
+ List.map2 (intern_cases_pattern genv scopes ([],[])) argscs pl in
+ let (ids',pll) = product_of_cases_patterns ids idslpl in
+ let pl' = List.map (fun (subst,pl) ->
+ (subst, PatCstr (loc,c,pl0@pl,alias_of aliases))) pll in
+ ids',pl'
+ | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)])
+ when Bigint.is_strictly_pos p ->
+ let np = Numeral (Bigint.neg p) in
+ intern_cases_pattern genv scopes aliases tmp_scope (CPatPrim(loc,np))
| CPatNotation (_,"( _ )",[a]) ->
- intern_cases_pattern scopes aliases tmp_scope a
+ intern_cases_pattern genv scopes aliases tmp_scope a
| CPatNotation (loc, ntn, args) ->
let ntn,args = contract_pat_notation ntn args in
let scopes = option_cons tmp_scope scopes in
- let ((ids,c),df) = Symbols.interp_notation loc ntn scopes in
- if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df;
+ let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+ if !dump then dump_notation_location (patntn_loc loc args ntn) df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
- subst_cases_pattern loc aliases intern_cases_pattern subst scopes c
- | CPatNumeral (loc, n) ->
+ subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes
+ c
+ | CPatPrim (loc, p) ->
let scopes = option_cons tmp_scope scopes in
- ([aliases],
- Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes)
+ let a = alias_of aliases in
+ let (c,df) = Notation.interp_prim_token_cases_pattern loc p a scopes in
+ if !dump then dump_notation_location (fst (unloc loc)) df;
+ (ids,[subst,c])
| CPatDelimiters (loc, key, e) ->
- intern_cases_pattern (find_delimiters_scope loc key::scopes)
+ intern_cases_pattern genv (find_delimiters_scope loc key::scopes)
aliases None e
| CPatAtom (loc, Some head) ->
(match maybe_constructor head with
| ConstrPat (c,args) ->
- ([aliases], PatCstr (loc,c,args,alias_of aliases))
+ check_constructor_length genv loc c [] [];
+ (ids,[subst, PatCstr (loc,c,args,alias_of aliases)])
| VarPat id ->
- let aliases = merge_aliases aliases id in
- ([aliases], PatVar (loc,alias_of aliases)))
+ let ids,subst = merge_aliases aliases id in
+ (ids,[subst, PatVar (loc,alias_of (ids,subst))]))
| CPatAtom (loc, None) ->
- ([aliases], PatVar (loc,alias_of aliases))
+ (ids,[subst, PatVar (loc,alias_of aliases)])
+ | CPatOr (loc, pl) ->
+ assert (pl <> []);
+ let pl' =
+ List.map (intern_cases_pattern genv scopes aliases tmp_scope) pl in
+ let (idsl,pl') = List.split pl' in
+ let ids = List.hd idsl in
+ check_or_pat_variables loc ids (List.tl idsl);
+ (ids,List.flatten pl')
(**********************************************************************)
(* Fix and CoFix *)
@@ -593,10 +616,10 @@ let locate_if_isevar loc na = function
(try match na with
| Name id -> Reserve.find_reserved_type id
| Anonymous -> raise Not_found
- with Not_found -> RHole (loc, BinderType na))
+ with Not_found -> RHole (loc, Evd.BinderType na))
| x -> x
-let check_hidden_implicit_parameters id (_,_,_,indnames,_) =
+let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
if List.mem id indnames then
errorlabstrm "" (str "A parameter or name of an inductive type " ++
pr_id id ++ str " must not be used as a bound variable in the type \
@@ -624,8 +647,8 @@ let check_projection isproj nargs r =
| RRef (loc, ref), Some _ ->
(try
let n = Recordops.find_projection_nparams ref + 1 in
- if nargs < n then
- user_err_loc (loc,"",str "Projection has not enough parameters");
+ if nargs <> n then
+ user_err_loc (loc,"",str "Projection has not the right number of explicit parameters");
with Not_found ->
user_err_loc
(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection"))
@@ -633,12 +656,11 @@ let check_projection isproj nargs r =
| _, None -> ()
let get_implicit_name n imps =
- if !Options.v7 then None
- else Some (Impargs.name_of_implicit (List.nth imps (n-1)))
+ Some (Impargs.name_of_implicit (List.nth imps (n-1)))
let set_hole_implicit i = function
- | RRef (loc,r) -> (loc,ImplicitArg (r,i))
- | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
+ | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
+ | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i))
| _ -> anomaly "Only refs have implicits"
let exists_implicit_name id =
@@ -679,18 +701,12 @@ let extract_explicit_arg imps args =
(**********************************************************************)
(* Syntax extensions *)
-let coerce_to_id = function
- | CRef (Ident (_,id)) -> id
- | c ->
- user_err_loc (constr_loc c, "subst_rawconstr",
- str"This expression should be a simple identifier")
-
let traverse_binder subst id (ids,tmpsc,scopes as env) =
try
(* Binders bound in the notation are consider first-order object *)
(* and binders not bound in the notation do not capture variables *)
(* outside the notation *)
- let id' = coerce_to_id (fst (List.assoc id subst)) in
+ let _,id' = coerce_to_id (fst (List.assoc id subst)) in
id', (Idset.add id' ids,tmpsc,scopes)
with Not_found ->
id, env
@@ -703,7 +719,7 @@ let rec subst_iterator y t = function
| RVar (_,id) as x -> if id = y then t else x
| x -> map_rawconstr (subst_iterator y t) x
-let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) =
+let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) =
function
| AVar id ->
begin
@@ -739,13 +755,13 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) =
let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
let ntn,args = contract_notation ntn args in
let scopes = option_cons tmp_scope scopes in
- let ((ids,c),df) = Symbols.interp_notation loc ntn scopes in
- if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df;
+ let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+ if !dump then dump_notation_location (ntn_loc loc args ntn) df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
subst_aconstr_in_rawconstr loc intern subst env c
let set_type_scope (ids,tmp_scope,scopes) =
- (ids,Some Symbols.type_scope,scopes)
+ (ids,Some Notation.type_scope,scopes)
let reset_tmp_scope (ids,tmp_scope,scopes) =
(ids,None,scopes)
@@ -753,7 +769,7 @@ let reset_tmp_scope (ids,tmp_scope,scopes) =
(**********************************************************************)
(* Main loop *)
-let internalise sigma env allow_soapp lvar c =
+let internalise sigma globalenv env allow_soapp lvar c =
let rec intern (ids,tmp_scope,scopes as env) = function
| CRef ref as x ->
let (c,imp,subscopes,l) = intern_reference env lvar ref in
@@ -769,20 +785,30 @@ let internalise sigma env allow_soapp lvar c =
with Not_found ->
raise (InternalisationError (locid,UnboundFixName (false,iddef)))
in
- let ids' = List.fold_right Idset.add lf ids in
let idl = Array.map
- (fun (id,n,bl,ty,bd) ->
- let ((ids'',_,_),rbl) =
- List.fold_left intern_local_binder (env,[]) bl in
- let ids''' = List.fold_right Idset.add lf ids'' in
- (List.rev rbl,
- intern_type (ids'',tmp_scope,scopes) ty,
- intern (ids''',None,scopes) bd)) dl in
- RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
+ (fun (id,(n,order),bl,ty,bd) ->
+ let ro, ((ids',_,_),rbl) =
+ (match order with
+ CStructRec ->
+ RStructRec,
+ List.fold_left intern_local_binder (env,[]) bl
+ | CWfRec c ->
+ let before, after = list_chop (succ n) bl in
+ let ((ids',_,_),rafter) =
+ List.fold_left intern_local_binder (env,[]) after in
+ let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
+ ro, List.fold_left intern_local_binder (env,rafter) before)
+ in
+ let ids'' = List.fold_right Idset.add lf ids' in
+ ((n, ro), List.rev rbl,
+ intern_type (ids',tmp_scope,scopes) ty,
+ intern (ids'',None,scopes) bd)) dl in
+ RRec (loc,RFix
+ (Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
- Array.map (fun (bl,_,_) -> bl) idl,
- Array.map (fun (_,ty,_) -> ty) idl,
- Array.map (fun (_,_,bd) -> bd) idl)
+ Array.map (fun (_,bl,_,_) -> bl) idl,
+ Array.map (fun (_,_,ty,_) -> ty) idl,
+ Array.map (fun (_,_,_,bd) -> bd) idl)
| CCoFix (loc, (locid,iddef), dl) ->
let lf = List.map (fun (id,_,_,_) -> id) dl in
let dl = Array.of_list dl in
@@ -792,15 +818,14 @@ let internalise sigma env allow_soapp lvar c =
with Not_found ->
raise (InternalisationError (locid,UnboundFixName (true,iddef)))
in
- let ids' = List.fold_right Idset.add lf ids in
let idl = Array.map
(fun (id,bl,ty,bd) ->
- let ((ids'',_,_),rbl) =
+ let ((ids',_,_),rbl) =
List.fold_left intern_local_binder (env,[]) bl in
- let ids''' = List.fold_right Idset.add lf ids'' in
+ let ids'' = List.fold_right Idset.add lf ids' in
(List.rev rbl,
- intern_type (ids'',tmp_scope,scopes) ty,
- intern (ids''',None,scopes) bd)) dl in
+ intern_type (ids',tmp_scope,scopes) ty,
+ intern (ids'',None,scopes) bd)) dl in
RRec (loc,RCoFix n,
Array.of_list lf,
Array.map (fun (bl,_,_) -> bl) idl,
@@ -819,15 +844,17 @@ let internalise sigma env allow_soapp lvar c =
| CLetIn (loc,(_,na),c1,c2) ->
RLetIn (loc, na, intern (reset_tmp_scope env) c1,
intern (push_name_env lvar env na) c2)
- | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) ->
- let scopes = option_cons tmp_scope scopes in
- Symbols.interp_numeral loc (Bignat.NEG p) scopes
+ | CNotation (loc,"- _",[CPrim (_,Numeral p)])
+ when Bigint.is_strictly_pos p ->
+ intern env (CPrim (loc,Numeral (Bigint.neg p)))
| CNotation (_,"( _ )",[a]) -> intern env a
| CNotation (loc,ntn,args) ->
intern_notation intern env loc ntn args
- | CNumeral (loc, n) ->
+ | CPrim (loc, p) ->
let scopes = option_cons tmp_scope scopes in
- Symbols.interp_numeral loc n scopes
+ let c,df = Notation.interp_prim_token loc p scopes in
+ if !dump then dump_notation_location (fst (unloc loc)) df;
+ c
| CDelimiters (loc, key, e) ->
intern (ids,None,find_delimiters_scope loc key::scopes) e
| CAppExpl (loc, (isproj,ref), args) ->
@@ -847,26 +874,22 @@ let internalise sigma env allow_soapp lvar c =
let c = intern_notation intern env loc ntn [] in
find_appl_head_data lvar c
| x -> (intern env f,[],[],[]) in
- let args = intern_impargs c env impargs args_scopes (merge_impargs l args) in
+ let args =
+ intern_impargs c env impargs args_scopes (merge_impargs l args) in
check_projection isproj (List.length args) c;
(match c with
(* Now compact "(f args') args" *)
| RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
| _ -> RApp (loc, c, args))
- | CCases (loc, (po,rtnpo), tms, eqns) ->
+ | CCases (loc, rtnpo, tms, eqns) ->
let tms,env' = List.fold_right
(fun citm (inds,env) ->
let (tm,ind),nal = intern_case_item env citm in
- (tm,ref ind)::inds,List.fold_left (push_name_env lvar) env nal)
+ (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
tms ([],env) in
let rtnpo = option_app (intern_type env') rtnpo in
- RCases (loc, (option_app (intern_type env) po, ref rtnpo), tms,
- List.map (intern_eqn (List.length tms) env) eqns)
- | COrderedCase (loc, tag, po, c, cl) ->
- let env = reset_tmp_scope env in
- ROrderedCase (loc, tag, option_app (intern_type env) po,
- intern env c,
- Array.of_list (List.map (intern env) cl),ref None)
+ let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
+ RCases (loc, rtnpo, tms, List.flatten eqns')
| CLetTuple (loc, nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
@@ -881,58 +904,52 @@ let internalise sigma env allow_soapp lvar c =
let p' = option_app (intern_type env'') po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole loc ->
- RHole (loc, QuestionMark)
+ RHole (loc, Evd.QuestionMark)
| CPatVar (loc, n) when allow_soapp ->
RPatVar (loc, n)
- | CPatVar (loc, (false,n)) when Options.do_translate () ->
- RVar (loc, n)
- | CPatVar (loc, (false,n as x)) ->
- if List.mem n (fst (let (a,_,_,_,_) = lvar in a)) & !Options.v7 then
- RVar (loc, n)
- else
- error_unbound_patvar loc n
+ | CPatVar (loc, (false,n)) ->
+ error_unbound_patvar loc n
| CPatVar (loc, _) ->
raise (InternalisationError (loc,NegativeMetavariable))
| CEvar (loc, n) ->
REvar (loc, n, None)
| CSort (loc, s) ->
RSort(loc,s)
- | CCast (loc, c1, c2) ->
- RCast (loc,intern env c1,intern_type env c2)
+ | CCast (loc, c1, k, c2) ->
+ RCast (loc,intern env c1,k,intern_type env c2)
| CDynamic (loc,d) -> RDynamic (loc,d)
and intern_type (ids,_,scopes) =
- intern (ids,Some Symbols.type_scope,scopes)
+ intern (ids,Some Notation.type_scope,scopes)
and intern_local_binder ((ids,ts,sc as env),bl) = function
- LocalRawAssum(nal,ty) ->
- let (loc,na) = List.hd nal in
- (* TODO: fail if several names with different implicit types *)
- let ty = locate_if_isevar loc na (intern_type env ty) in
+ | LocalRawAssum(nal,ty) ->
+ let (loc,na) = List.hd nal in
+ (* TODO: fail if several names with different implicit types *)
+ let ty = locate_if_isevar loc na (intern_type env ty) in
List.fold_left
(fun ((ids,ts,sc),bl) (_,na) ->
((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl))
(env,bl) nal
| LocalRawDef((loc,na),def) ->
((name_fold Idset.add na ids,ts,sc),
- (na,Some(intern env def),RHole(loc,BinderType na))::bl)
-
- and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) =
- let (idsl_substl_list,pl) =
- List.split
- (List.map (intern_cases_pattern scopes ([],[]) None) lhs) in
- let idsl, substl = List.split (List.flatten idsl_substl_list) in
- let eqn_ids = List.flatten idsl in
- let subst = List.flatten substl in
- (* Linearity implies the order in ids is irrelevant *)
- check_linearity lhs eqn_ids;
- check_uppercase loc eqn_ids;
- check_number_of_pattern loc n pl;
- let rhs = replace_vars_constr_expr subst rhs in
- List.iter message_redundant_alias subst;
- let env_ids = List.fold_right Idset.add eqn_ids ids in
- (loc, eqn_ids,pl,intern (env_ids,tmp_scope,scopes) rhs)
+ (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+
+ and intern_eqn n (ids,tmp_scope,scopes as _env) (loc,lhs,rhs) =
+ let idsl_pll =
+ List.map (intern_cases_pattern globalenv scopes ([],[]) None) lhs in
+
+ let eqn_ids,pll = product_of_cases_patterns [] idsl_pll in
+ (* Linearity implies the order in ids is irrelevant *)
+ check_linearity lhs eqn_ids;
+ check_number_of_pattern loc n (snd (List.hd pll));
+ let env_ids = List.fold_right Idset.add eqn_ids ids in
+ List.map (fun (subst,pl) ->
+ let rhs = replace_vars_constr_expr subst rhs in
+ List.iter message_redundant_alias subst;
+ let rhs' = intern (env_ids,tmp_scope,scopes) rhs in
+ (loc,eqn_ids,pl,rhs')) pll
and intern_case_item (vars,_,scopes as env) (tm,(na,t)) =
let tm' = intern env tm in
@@ -941,21 +958,23 @@ let internalise sigma env allow_soapp lvar c =
let tids = names_of_cases_indtype t in
let tids = List.fold_right Idset.add tids Idset.empty in
let t = intern_type (tids,None,scopes) t in
- begin match t with
- | RRef (loc,IndRef ind) -> [],Some (loc,ind,[])
+ let (_,_,nal as indsign) =
+ match t with
+ | RRef (loc,IndRef ind) -> (loc,ind,[])
| RApp (loc,RRef (_,IndRef ind),l) ->
let nal = List.map (function
| RHole _ -> Anonymous
| RVar (_,id) -> Name id
| c ->
user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
- nal, Some (loc,ind,nal)
- | _ -> error_bad_inductive_type (loc_of_rawconstr t)
- end
+ (loc,ind,nal)
+ | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
+ check_inductive_length globalenv indsign;
+ nal, Some indsign
| None ->
[], None in
let na = match tm', na with
- | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id
+ | RVar (_,id), None when Idset.mem id vars -> Name id
| _, None -> Anonymous
| _, Some na -> na in
(tm',(na,typ)), na::ids
@@ -1032,114 +1051,53 @@ let extract_ids env =
(Termops.ids_of_rel_context (Environ.rel_context env))
Idset.empty
-let interp_rawconstr_gen_with_implicits isarity sigma env (indpars,impls) allow_soapp ltacvar c =
- let tmp_scope = if isarity then Some Symbols.type_scope else None in
- internalise sigma (extract_ids env, tmp_scope,[])
- allow_soapp (ltacvar,Environ.named_context env, [], indpars, impls) c
-
-let interp_rawconstr_gen isarity sigma env allow_soapp ltacvar c =
- interp_rawconstr_gen_with_implicits isarity sigma env ([],[]) allow_soapp ltacvar c
-
-let interp_rawconstr sigma env c =
- interp_rawconstr_gen false sigma env false ([],[]) c
-
-let interp_rawtype sigma env c =
- interp_rawconstr_gen true sigma env false ([],[]) c
+let intern_gen isarity sigma env
+ ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+ c =
+ let tmp_scope = if isarity then Some Notation.type_scope else None in
+ internalise sigma env (extract_ids env, tmp_scope,[])
+ allow_soapp (ltacvars,Environ.named_context env, [], impls) c
-let interp_rawtype_with_implicits sigma env impls c =
- interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c
+let intern_constr sigma env c = intern_gen false sigma env c
-let interp_rawconstr_with_implicits sigma env vars impls c =
- interp_rawconstr_gen_with_implicits false sigma env ([],impls) false
- (vars,[]) c
-
-(*
-(* The same as interp_rawconstr but with a list of variables which must not be
- globalized *)
-
-let interp_rawconstr_wo_glob sigma env lvar c =
- interp_rawconstr_gen sigma env [] (Some []) lvar c
-*)
+let intern_ltac isarity ltacvars sigma env c =
+ intern_gen isarity sigma env ~ltacvars:ltacvars c
(*********************************************************************)
(* Functions to parse and interpret constructions *)
-let interp_constr sigma env c =
- understand sigma env (interp_rawconstr sigma env c)
-
-let interp_openconstr sigma env c =
- understand_gen_tcc sigma env [] None (interp_rawconstr sigma env c)
-
-let interp_casted_openconstr sigma env c typ =
- understand_gen_tcc sigma env [] (Some typ) (interp_rawconstr sigma env c)
-
-let interp_type sigma env c =
- understand_type sigma env (interp_rawtype sigma env c)
-
-let interp_binder sigma env na t =
- let t = interp_rawtype sigma env t in
- understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
-
-let interp_type_with_implicits sigma env impls c =
- understand_type sigma env (interp_rawtype_with_implicits sigma env impls c)
+let interp_gen kind sigma env
+ ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+ c =
+ Default.understand_gen kind sigma env
+ (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c)
-let judgment_of_rawconstr sigma env c =
- understand_judgment sigma env (interp_rawconstr sigma env c)
-
-let type_judgment_of_rawconstr sigma env c =
- understand_type_judgment sigma env (interp_rawconstr sigma env c)
-
-(* To retype a list of key*constr with undefined key *)
-let retype_list sigma env lst =
- List.fold_right (fun (x,csr) a ->
- try (x,Retyping.get_judgment_of env sigma csr)::a with
- | Anomaly _ -> a) lst []
-
-(* List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
-
-type ltac_sign =
- identifier list * (identifier * identifier option) list
-
-type ltac_env =
- (identifier * Term.constr) list * (identifier * identifier option) list
+let interp_constr sigma env c =
+ interp_gen (OfType None) sigma env c
-(* Interprets a constr according to two lists *)
-(* of instantiations (variables and metas) *)
-(* Note: typ is retyped *)
-let interp_constr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
- let c = interp_rawconstr_gen false sigma env false
- (List.map fst ltacvars,unbndltacvars) c in
- let typs = retype_list sigma env ltacvars in
- understand_gen sigma env typs exptyp c
+let interp_type sigma env ?(impls=([],[])) c =
+ interp_gen IsType sigma env ~impls c
-(*Interprets a casted constr according to two lists of instantiations
- (variables and metas)*)
-let interp_openconstr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
- let c = interp_rawconstr_gen false sigma env false
- (List.map fst ltacvars,unbndltacvars) c in
- let typs = retype_list sigma env ltacvars in
- understand_gen_tcc sigma env typs exptyp c
+let interp_casted_constr sigma env ?(impls=([],[])) c typ =
+ interp_gen (OfType (Some typ)) sigma env ~impls c
-let interp_casted_constr sigma env c typ =
- understand_gen sigma env [] (Some typ) (interp_rawconstr sigma env c)
+let interp_open_constr sigma env c =
+ Default.understand_tcc sigma env (intern_constr sigma env c)
-let interp_casted_constr_with_implicits sigma env impls c typ =
- understand_gen sigma env [] (Some typ)
- (interp_rawconstr_with_implicits sigma env [] impls c)
+let interp_constr_judgment sigma env c =
+ Default.understand_judgment sigma env (intern_constr sigma env c)
-let interp_constrpattern_gen sigma env ltacvar c =
- let c = interp_rawconstr_gen false sigma env true (ltacvar,[]) c in
- pattern_of_rawconstr c
+type ltac_sign = identifier list * unbound_ltac_var_map
let interp_constrpattern sigma env c =
- interp_constrpattern_gen sigma env [] c
+ pattern_of_rawconstr (intern_gen false sigma env ~allow_soapp:true c)
let interp_aconstr impls vars a =
let env = Global.env () in
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = List.map (fun id -> (id,ref None)) vars in
- let c = internalise Evd.empty (extract_ids env, None, [])
- false (([],[]),Environ.named_context env,vl,[],impls) a in
+ let c = internalise Evd.empty (Global.env()) (extract_ids env, None, [])
+ false (([],[]),Environ.named_context env,vl,([],impls)) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a = aconstr_of_rawconstr vars c in
(* Returns [a] and the ordered list of variables with their scopes *)
@@ -1148,6 +1106,33 @@ let interp_aconstr impls vars a =
(fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
a
+(* Interpret binders and contexts *)
+
+let interp_binder sigma env na t =
+ let t = intern_gen true sigma env t in
+ Default.understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
+
+open Environ
+open Term
+
+let interp_context sigma env params =
+ List.fold_left
+ (fun (env,params) d -> match d with
+ | LocalRawAssum ([_,na],(CHole _ as t)) ->
+ let t = interp_binder sigma env na t in
+ let d = (na,None,t) in
+ (push_rel d env, d::params)
+ | LocalRawAssum (nal,t) ->
+ let t = interp_type sigma env t in
+ let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+ let ctx = List.rev ctx in
+ (push_rel_context ctx env, ctx@params)
+ | LocalRawDef ((_,na),c) ->
+ let c = interp_constr_judgment sigma env c in
+ let d = (na, Some c.uj_val, c.uj_type) in
+ (push_rel d env,d::params))
+ (env,[]) params
+
(**********************************************************************)
(* Locating reference, possibly via an abbreviation *)
@@ -1166,7 +1151,7 @@ let is_global id =
false
let global_reference id =
- constr_of_reference (locate_reference (make_short_qualid id))
+ constr_of_global (locate_reference (make_short_qualid id))
let construct_reference ctx id =
try
@@ -1175,5 +1160,5 @@ let construct_reference ctx id =
global_reference id
let global_reference_in_absolute_module dir id =
- constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id))
+ constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id))
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 06039da7..cdd87a7c 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrintern.mli,v 1.15.2.2 2005/01/21 16:41:50 herbelin Exp $ i*)
+(*i $Id: constrintern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
(*i*)
open Names
@@ -17,9 +17,9 @@ open Environ
open Libnames
open Rawterm
open Pattern
-open Coqast
open Topconstr
open Termops
+open Pretyping
(*i*)
(*s Translation from front abstract syntax of term to untyped terms (rawconstr)
@@ -34,73 +34,67 @@ open Termops
*)
(* To interpret implicits and arg scopes of recursive variables in
- inductive types and recursive definitions *)
+ inductive types and recursive definitions; mention of a list of
+ implicits arguments in the ``rel'' part of [env]; the second
+ argument associates a list of implicit positions and scopes to
+ identifiers declared in the [rel_context] of [env] *)
+
type var_internalisation_data =
identifier list * Impargs.implicits_list * scope_name option list
type implicits_env = (identifier * var_internalisation_data) list
type full_implicits_env = identifier list * implicits_env
-type ltac_sign =
- identifier list * (identifier * identifier option) list
-
-type ltac_env =
- (identifier * constr) list * (identifier * identifier option) list
-
-(* Interprets global names, including syntactic defs and section variables *)
-val interp_rawconstr : evar_map -> env -> constr_expr -> rawconstr
-val interp_rawconstr_gen : bool -> evar_map -> env ->
- bool -> ltac_sign -> constr_expr -> rawconstr
-
-(*s Composing the translation with typing *)
-val interp_constr : evar_map -> env -> constr_expr -> constr
-val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr
-val interp_type : evar_map -> env -> constr_expr -> types
-val interp_binder : evar_map -> env -> name -> constr_expr -> types
-val interp_openconstr : evar_map -> env -> constr_expr -> evar_map * constr
-val interp_casted_openconstr :
- evar_map -> env -> constr_expr -> constr -> evar_map * constr
-
-(* [interp_type_with_implicits] extends [interp_type] by allowing
- implicits arguments in the ``rel'' part of [env]; the extra
- argument associates a list of implicit positions to identifiers
- declared in the [rel_context] of [env] *)
-val interp_type_with_implicits :
- evar_map -> env -> full_implicits_env -> constr_expr -> types
-
-val interp_casted_constr_with_implicits :
- evar_map -> env -> implicits_env -> constr_expr -> types -> constr
-
-val interp_rawconstr_with_implicits :
- evar_map -> env -> identifier list -> implicits_env -> constr_expr ->
- rawconstr
-
-(*s Build a judgement from *)
-val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
-val type_judgment_of_rawconstr :
- evar_map -> env -> constr_expr -> unsafe_type_judgment
-
-(* Interprets a constr according to two lists of instantiations (variables and
- metas), possibly casting it*)
-val interp_constr_gen :
- evar_map -> env -> ltac_env -> constr_expr -> constr option -> constr
-
-(* Interprets a constr according to two lists of instantiations (variables and
- metas), possibly casting it, and turning unresolved evar into metas*)
-val interp_openconstr_gen :
- evar_map -> env -> ltac_env ->
- constr_expr -> constr option -> evar_map * constr
-
-(* Interprets constr patterns according to a list of instantiations
- (variables)*)
-val interp_constrpattern_gen : evar_map -> env -> identifier list ->
- constr_expr -> patvar list * constr_pattern
+type ltac_sign = identifier list * unbound_ltac_var_map
+
+(*s Internalisation performs interpretation of global names and notations *)
+
+val intern_constr : evar_map -> env -> constr_expr -> rawconstr
+
+val intern_gen : bool -> evar_map -> env ->
+ ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+ constr_expr -> rawconstr
+
+(*s Composing internalisation with pretyping *)
+
+(* Main interpretation function *)
+
+val interp_gen : typing_constraint -> evar_map -> env ->
+ ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+ constr_expr -> constr
+
+(* Particular instances *)
+
+val interp_constr : evar_map -> env ->
+ constr_expr -> constr
+
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
+ constr_expr -> types -> constr
+
+val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
+ constr_expr -> types
+
+val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
+
+(*s Build a judgment *)
+
+val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
+
+(* Interprets constr patterns *)
val interp_constrpattern :
evar_map -> env -> constr_expr -> patvar list * constr_pattern
val interp_reference : ltac_sign -> reference -> rawconstr
+(* Interpret binders *)
+
+val interp_binder : evar_map -> env -> name -> constr_expr -> types
+
+(* Interpret contexts: returns extended env and context *)
+
+val interp_context : evar_map -> env -> local_binder list -> env * rel_context
+
(* Locating references of constructions, possibly via a syntactic definition *)
val locate_reference : qualid -> global_reference
@@ -110,6 +104,7 @@ val global_reference : identifier -> constr
val global_reference_in_absolute_module : dir_path -> identifier -> constr
(* Interprets into a abbreviatable constr *)
+
val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
interpretation
@@ -120,7 +115,3 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
type coqdoc_state
val coqdoc_freeze : unit -> coqdoc_state
val coqdoc_unfreeze : coqdoc_state -> unit
-
-(* For v8 translation *)
-val set_temporary_implicits_in :
- (identifier * Impargs.implicits_list) list -> unit
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 8ce9bfaf..afee83e8 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml,v 1.14.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(* $Id: coqlib.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
open Util
open Pp
@@ -16,19 +16,25 @@ open Libnames
open Pattern
open Nametab
+(************************************************************************)
+(* Generic functions to find Coq objects *)
+
+type message = string
+
let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let gen_reference locstr dir s =
- let dir = make_dir ("Coq"::dir) in
- let id = Constrextern.id_of_v7_string s in
- let sp = Libnames.make_path dir id in
+let find_reference locstr dir s =
+ let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
try
Nametab.absolute_reference sp
with Not_found ->
anomaly (locstr^": cannot find "^(string_of_path sp))
-
-let gen_constant locstr dir s =
- constr_of_reference (gen_reference locstr dir s)
+
+let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
+let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
+
+let gen_reference = coq_reference
+let gen_constant = coq_constant
let list_try_find f =
let rec try_find_f = function
@@ -43,11 +49,11 @@ let has_suffix_in_dirs dirs ref =
let gen_constant_in_modules locstr dirs s =
let dirs = List.map make_dir dirs in
- let id = Constrextern.id_of_v7_string s in
+ let id = id_of_string s in
let all = Nametab.locate_all (make_short_qualid id) in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
- | [x] -> constr_of_reference x
+ | [x] -> constr_of_global x
| [] ->
anomalylabstrm "" (str (locstr^": cannot find "^s^
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
@@ -58,9 +64,27 @@ let gen_constant_in_modules locstr dirs s =
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
prlist_with_sep pr_coma pr_dirpath dirs)
-let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s
-let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s
+(* For tactics/commands requiring vernacular libraries *)
+
+let check_required_library d =
+ let d' = List.map id_of_string d in
+ let dir = make_dirpath (List.rev d') in
+ if not (Library.library_is_loaded dir) then
+(* Loading silently ...
+ let m, prefix = list_sep_last d' in
+ read_library
+ (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
+*)
+(* or failing ...*)
+ error ("Library "^(list_last d)^" has to be required first")
+
+(************************************************************************)
+(* Specific Coq objects *)
+
+let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
+
+let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
let arith_dir = ["Coq";"Arith"]
let arith_modules = [arith_dir]
@@ -91,22 +115,33 @@ let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
let arith_module = make_dir ["Coq";"Arith";"Arith"]
(* TODO: temporary hack *)
-let make_path dir id = Libnames.encode_kn dir id
+let make_kn dir id = Libnames.encode_kn dir id
-let nat_path = make_path datatypes_module (id_of_string "nat")
+(** Natural numbers *)
+let nat_kn = make_kn datatypes_module (id_of_string "nat")
+let nat_path = Libnames.make_path datatypes_module (id_of_string "nat")
-let glob_nat = IndRef (nat_path,0)
+let glob_nat = IndRef (nat_kn,0)
-let path_of_O = ((nat_path,0),1)
-let path_of_S = ((nat_path,0),2)
+let path_of_O = ((nat_kn,0),1)
+let path_of_S = ((nat_kn,0),2)
let glob_O = ConstructRef path_of_O
let glob_S = ConstructRef path_of_S
-let eq_path = make_path logic_module (id_of_string "eq")
-let eqT_path = make_path logic_module (id_of_string "eq")
+(** Booleans *)
+let bool_kn = make_kn datatypes_module (id_of_string "bool")
+
+let glob_bool = IndRef (bool_kn,0)
-let glob_eq = IndRef (eq_path,0)
-let glob_eqT = IndRef (eqT_path,0)
+let path_of_true = ((bool_kn,0),1)
+let path_of_false = ((bool_kn,0),2)
+let glob_true = ConstructRef path_of_true
+let glob_false = ConstructRef path_of_false
+
+(** Equality *)
+let eq_kn = make_kn logic_module (id_of_string "eq")
+
+let glob_eq = IndRef (eq_kn,0)
type coq_sigma_data = {
proj1 : constr;
@@ -131,6 +166,13 @@ let build_sigma_type () =
intro = init_constant ["Specif"] "existT";
typ = init_constant ["Specif"] "sigT" }
+let build_prod () =
+ { proj1 = init_constant ["Datatypes"] "fst";
+ proj2 = init_constant ["Datatypes"] "snd";
+ elim = init_constant ["Datatypes"] "prod_rec";
+ intro = init_constant ["Datatypes"] "pair";
+ typ = init_constant ["Datatypes"] "prod" }
+
(* Equalities *)
type coq_leibniz_eq_data = {
eq : constr;
@@ -160,9 +202,10 @@ let build_coq_eq_data () = {
rrec = Some (Lazy.force coq_eq_rec);
rect = Some (Lazy.force coq_eq_rect);
congr = Lazy.force coq_eq_congr;
- sym = Lazy.force coq_eq_sym }
+ sym = Lazy.force coq_eq_sym }
let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_sym_eq () = Lazy.force coq_eq_sym
let build_coq_f_equal2 () = Lazy.force coq_f_equal2
(* Specif *)
@@ -170,56 +213,23 @@ let coq_sumbool = lazy_init_constant ["Specif"] "sumbool"
let build_coq_sumbool () = Lazy.force coq_sumbool
-(* Equality on Type *)
-
-let coq_eqT_eq = lazy_init_constant ["Logic"] "eq"
-let coq_eqT_refl = lazy_init_constant ["Logic"] "refl_equal"
-let coq_eqT_ind = lazy_init_constant ["Logic"] "eq_ind"
-let coq_eqT_congr =lazy_init_constant ["Logic"] "f_equal"
-let coq_eqT_sym = lazy_init_constant ["Logic"] "sym_eq"
-
-let build_coq_eqT_data () = {
- eq = Lazy.force coq_eqT_eq;
- refl = Lazy.force coq_eqT_refl;
- ind = Lazy.force coq_eqT_ind;
- rrec = None;
- rect = None;
- congr = Lazy.force coq_eqT_congr;
- sym = Lazy.force coq_eqT_sym }
-
-let build_coq_eqT () = Lazy.force coq_eqT_eq
-let build_coq_sym_eqT () = Lazy.force coq_eqT_sym
-
(* Equality on Type as a Type *)
-let coq_idT_eq = lazy_init_constant ["Datatypes"] "identity"
-let coq_idT_refl = lazy_init_constant ["Datatypes"] "refl_identity"
-let coq_idT_ind = lazy_init_constant ["Datatypes"] "identity_ind"
-let coq_idT_rec = lazy_init_constant ["Datatypes"] "identity_rec"
-let coq_idT_rect = lazy_init_constant ["Datatypes"] "identity_rect"
-let coq_idT_congr = lazy_init_constant ["Logic_Type"] "congr_id"
-let coq_idT_sym = lazy_init_constant ["Logic_Type"] "sym_id"
-
-let build_coq_idT_data () = {
- eq = Lazy.force coq_idT_eq;
- refl = Lazy.force coq_idT_refl;
- ind = Lazy.force coq_idT_ind;
- rrec = Some (Lazy.force coq_idT_rec);
- rect = Some (Lazy.force coq_idT_rect);
- congr = Lazy.force coq_idT_congr;
- sym = Lazy.force coq_idT_sym }
-
-let lazy_init_constant_v7 d id id7 =
- if !Options.v7 then lazy_init_constant d id else
- lazy (anomaly
- (id7^" does no longer exist in V8 new syntax, use "^id
- ^" instead (probably an error in ML contributed code)"))
-
-(* Empty Type *)
-let coq_EmptyT = lazy_init_constant_v7 ["Logic"] "False" "EmptyT"
-
-(* Unit Type and its unique inhabitant *)
-let coq_UnitT = lazy_init_constant_v7 ["Datatypes"] "unit" "UnitT"
-let coq_IT = lazy_init_constant_v7 ["Datatypes"] "tt" "IT"
+let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
+let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
+let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
+let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
+let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
+let coq_identity_congr = lazy_init_constant ["Logic_Type"] "congr_id"
+let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id"
+
+let build_coq_identity_data () = {
+ eq = Lazy.force coq_identity_eq;
+ refl = Lazy.force coq_identity_refl;
+ ind = Lazy.force coq_identity_ind;
+ rrec = Some (Lazy.force coq_identity_rec);
+ rect = Some (Lazy.force coq_identity_rect);
+ congr = Lazy.force coq_identity_congr;
+ sym = Lazy.force coq_identity_sym }
(* The False proposition *)
let coq_False = lazy_init_constant ["Logic"] "False"
@@ -235,10 +245,6 @@ let coq_or = lazy_init_constant ["Logic"] "or"
let coq_ex = lazy_init_constant ["Logic"] "ex"
(* Runtime part *)
-let build_coq_EmptyT () = Lazy.force coq_EmptyT
-let build_coq_UnitT () = Lazy.force coq_UnitT
-let build_coq_IT () = Lazy.force coq_IT
-
let build_coq_True () = Lazy.force coq_True
let build_coq_I () = Lazy.force coq_I
@@ -248,47 +254,14 @@ let build_coq_and () = Lazy.force coq_and
let build_coq_or () = Lazy.force coq_or
let build_coq_ex () = Lazy.force coq_ex
-(****************************************************************************)
-(* Patterns *)
-(* This needs to have interp_constrpattern available ...
-
-let parse_constr s =
- try
- Pcoq.parse_string Pcoq.Constr.constr_eoi s
- with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
- error "Syntax error : not a construction"
-
-let parse_pattern s =
- Constrintern.interp_constrpattern Evd.empty (Global.env()) (parse_constr s)
-let coq_eq_pattern =
- lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
-let coq_eqT_pattern =
- lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
-let coq_idT_pattern =
- lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)"))
-let coq_existS_pattern =
- lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)"))
-let coq_existT_pattern =
- lazy (snd (parse_pattern "(Coq.Init.Specif.existT ?1 ?2 ?3 ?4)"))
-let coq_not_pattern =
- lazy (snd (parse_pattern "(Coq.Init.Logic.not ?)"))
-let coq_imp_False_pattern =
- lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
-let coq_imp_False_pattern =
- lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
-let coq_eqdec_partial_pattern =
- lazy (snd (parse_pattern "(sumbool (eq ?1 ?2 ?3) ?4)"))
-let coq_eqdec_pattern =
- lazy (snd (parse_pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
-*)
-
(* The following is less readable but does not depend on parsing *)
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
-let coq_eqT_ref = coq_eq_ref
-let coq_idT_ref = lazy (init_reference ["Datatypes"] "identity")
+let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
let coq_existS_ref = lazy (init_reference ["Specif"] "existS")
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
let coq_not_ref = lazy (init_reference ["Logic"] "not")
let coq_False_ref = lazy (init_reference ["Logic"] "False")
let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
+let coq_or_ref = lazy (init_reference ["Logic"] "or")
+
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 3b377f29..c81d72de 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqlib.mli,v 1.5.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: coqlib.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
(*i*)
open Names
@@ -19,11 +19,29 @@ open Pattern
(*s This module collects the global references, constructions and
patterns of the standard library used in ocaml files *)
-(*s Some utilities, the first argument is used for error messages.
- Must be used lazyly. s*)
+(*s [find_reference caller_message [dir;subdir;...] s] returns a global
+ reference to the name dir.subdir.(...).s; the corresponding module
+ must have been required or in the process of being compiled so that
+ it must be used lazyly; it raises an anomaly with the given message
+ if not found *)
-val gen_reference : string->string list -> string -> global_reference
-val gen_constant : string->string list -> string -> constr
+type message = string
+
+val find_reference : message -> string list -> string -> global_reference
+
+(* [coq_reference caller_message [dir;subdir;...] s] returns a
+ global reference to the name Coq.dir.subdir.(...).s *)
+
+val coq_reference : message -> string list -> string -> global_reference
+
+(* idem but return a term *)
+
+val coq_constant : message -> string list -> string -> constr
+
+(* Synonyms of [coq_constant] and [coq_reference] *)
+
+val gen_constant : message -> string list -> string -> constr
+val gen_reference : message -> string list -> string -> global_reference
(* Search in several modules (not prefixed by "Coq") *)
val gen_constant_in_modules : string->string list list-> string -> constr
@@ -31,6 +49,9 @@ val arith_modules : string list list
val zarith_base_modules : string list list
val init_modules : string list list
+(* For tactics/commands requiring vernacular libraries *)
+val check_required_library : string list -> unit
+
(*s Global references *)
(* Modules *)
@@ -38,15 +59,22 @@ val logic_module : dir_path
val logic_type_module : dir_path
(* Natural numbers *)
+val nat_path : section_path
val glob_nat : global_reference
val path_of_O : constructor
val path_of_S : constructor
val glob_O : global_reference
val glob_S : global_reference
+(* Booleans *)
+val glob_bool : global_reference
+val path_of_true : constructor
+val path_of_false : constructor
+val glob_true : global_reference
+val glob_false : global_reference
+
(* Equality *)
val glob_eq : global_reference
-val glob_eqT : global_reference
(*s Constructions and patterns related to Coq initial state are unknown
at compile time. Therefore, we can only provide methods to build
@@ -66,6 +94,8 @@ type coq_sigma_data = {
val build_sigma_set : coq_sigma_data delayed
val build_sigma_type : coq_sigma_data delayed
+(* Non-dependent pairs in Set from Datatypes *)
+val build_prod : coq_sigma_data delayed
type coq_leibniz_eq_data = {
eq : constr;
@@ -77,20 +107,11 @@ type coq_leibniz_eq_data = {
sym : constr }
val build_coq_eq_data : coq_leibniz_eq_data delayed
-val build_coq_eqT_data : coq_leibniz_eq_data delayed
-val build_coq_idT_data : coq_leibniz_eq_data delayed
+val build_coq_identity_data : coq_leibniz_eq_data delayed
-val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
+val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
+val build_coq_sym_eq : constr delayed (* = [(build_coq_eq_data()).sym] *)
val build_coq_f_equal2 : constr delayed
-val build_coq_eqT : constr delayed
-val build_coq_sym_eqT : constr delayed
-
-(* Empty Type *)
-val build_coq_EmptyT : constr delayed
-
-(* Unit Type and its unique inhabitant *)
-val build_coq_UnitT : constr delayed
-val build_coq_IT : constr delayed
(* Specif *)
val build_coq_sumbool : constr delayed
@@ -116,11 +137,12 @@ val build_coq_or : constr delayed
val build_coq_ex : constr delayed
val coq_eq_ref : global_reference lazy_t
-val coq_eqT_ref : global_reference lazy_t
-val coq_idT_ref : global_reference lazy_t
+val coq_identity_ref : global_reference lazy_t
val coq_existS_ref : global_reference lazy_t
val coq_existT_ref : global_reference lazy_t
val coq_not_ref : global_reference lazy_t
val coq_False_ref : global_reference lazy_t
val coq_sumbool_ref : global_reference lazy_t
val coq_sig_ref : global_reference lazy_t
+
+val coq_or_ref : global_reference lazy_t
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 7facebcc..511cf88a 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: genarg.ml,v 1.9.2.2 2005/01/15 14:56:54 herbelin Exp $ *)
+(* $Id: genarg.ml 7879 2006-01-16 13:58:09Z herbelin $ *)
open Pp
open Util
@@ -26,16 +26,15 @@ type argument_type =
| PreIdentArgType
| IntroPatternArgType
| IdentArgType
- | HypArgType
+ | VarArgType
| RefArgType
(* Specific types *)
| SortArgType
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
- | TacticArgType
- | OpenConstrArgType
- | CastedOpenConstrArgType
+ | TacticArgType of int
+ | OpenConstrArgType of bool
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
@@ -70,15 +69,17 @@ type intro_pattern_expr =
| IntroOrAndPattern of case_intro_pattern_expr
| IntroWildcard
| IntroIdentifier of identifier
+ | IntroAnonymous
and case_intro_pattern_expr = intro_pattern_expr list list
let rec pr_intro_pattern = function
| IntroOrAndPattern pll -> pr_case_intro_pattern pll
| IntroWildcard -> str "_"
| IntroIdentifier id -> pr_id id
+ | IntroAnonymous -> str "?"
and pr_case_intro_pattern = function
- | [_::_ as pl] ->
+ | [pl] ->
str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
| pll ->
str "[" ++
@@ -117,9 +118,9 @@ let rawwit_ident = IdentArgType
let globwit_ident = IdentArgType
let wit_ident = IdentArgType
-let rawwit_var = HypArgType
-let globwit_var = HypArgType
-let wit_var = HypArgType
+let rawwit_var = VarArgType
+let globwit_var = VarArgType
+let wit_var = VarArgType
let rawwit_ref = RefArgType
let globwit_ref = RefArgType
@@ -141,17 +142,21 @@ let rawwit_constr_may_eval = ConstrMayEvalArgType
let globwit_constr_may_eval = ConstrMayEvalArgType
let wit_constr_may_eval = ConstrMayEvalArgType
-let rawwit_tactic = TacticArgType
-let globwit_tactic = TacticArgType
-let wit_tactic = TacticArgType
+let rawwit_tactic n = TacticArgType n
+let globwit_tactic n = TacticArgType n
+let wit_tactic n = TacticArgType n
-let rawwit_open_constr = OpenConstrArgType
-let globwit_open_constr = OpenConstrArgType
-let wit_open_constr = OpenConstrArgType
+let rawwit_open_constr_gen b = OpenConstrArgType b
+let globwit_open_constr_gen b = OpenConstrArgType b
+let wit_open_constr_gen b = OpenConstrArgType b
-let rawwit_casted_open_constr = CastedOpenConstrArgType
-let globwit_casted_open_constr = CastedOpenConstrArgType
-let wit_casted_open_constr = CastedOpenConstrArgType
+let rawwit_open_constr = rawwit_open_constr_gen false
+let globwit_open_constr = globwit_open_constr_gen false
+let wit_open_constr = wit_open_constr_gen false
+
+let rawwit_casted_open_constr = rawwit_open_constr_gen true
+let globwit_casted_open_constr = globwit_open_constr_gen true
+let wit_casted_open_constr = wit_open_constr_gen true
let rawwit_constr_with_bindings = ConstrWithBindingsArgType
let globwit_constr_with_bindings = ConstrWithBindingsArgType
@@ -178,24 +183,24 @@ let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen"
let genarg_tag (s,_) = s
let fold_list0 f = function
- | (List0ArgType t as u, l) ->
+ | (List0ArgType t, l) ->
List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
| _ -> failwith "Genarg: not a list0"
let fold_list1 f = function
- | (List1ArgType t as u, l) ->
+ | (List1ArgType t, l) ->
List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
| _ -> failwith "Genarg: not a list1"
let fold_opt f a = function
- | (OptArgType t as u, l) ->
+ | (OptArgType t, l) ->
(match Obj.magic l with
| None -> a
| Some x -> f (in_gen t x))
| _ -> failwith "Genarg: not a opt"
let fold_pair f = function
- | (PairArgType (t1,t2) as u, l) ->
+ | (PairArgType (t1,t2), l) ->
let (x1,x2) = Obj.magic l in
f (in_gen t1 x1) (in_gen t2 x2)
| _ -> failwith "Genarg: not a pair"
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 967d5050..99de4ca4 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: genarg.mli,v 1.9.2.4 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: genarg.mli 7879 2006-01-16 13:58:09Z herbelin $ i*)
open Util
open Names
@@ -32,6 +32,7 @@ type intro_pattern_expr =
| IntroOrAndPattern of case_intro_pattern_expr
| IntroWildcard
| IntroIdentifier of identifier
+ | IntroAnonymous
and case_intro_pattern_expr = intro_pattern_expr list list
val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
@@ -114,7 +115,7 @@ val wit_ident : (identifier,'co,'ta) abstract_argument_type
val rawwit_var : (identifier located,'co,'ta) abstract_argument_type
val globwit_var : (identifier located,'co,'ta) abstract_argument_type
-val wit_var : ('co,'co,'ta) abstract_argument_type
+val wit_var : (identifier,'co,'ta) abstract_argument_type
val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
@@ -136,6 +137,10 @@ val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta)
val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
+val rawwit_open_constr_gen : bool -> (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr,constr,'ta) abstract_argument_type
+
val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type
@@ -157,9 +162,9 @@ val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short
val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
(* TODO: transformer tactic en extra arg *)
-val rawwit_tactic : ('ta,constr_expr,'ta) abstract_argument_type
-val globwit_tactic : ('ta,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_tactic : ('ta,constr,'ta) abstract_argument_type
+val rawwit_tactic : int -> ('ta,constr_expr,'ta) abstract_argument_type
+val globwit_tactic : int -> ('ta,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_tactic : int -> ('ta,constr,'ta) abstract_argument_type
val wit_list0 :
('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
@@ -227,16 +232,15 @@ type argument_type =
| PreIdentArgType
| IntroPatternArgType
| IdentArgType
- | HypArgType
+ | VarArgType
| RefArgType
(* Specific types *)
| SortArgType
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
- | TacticArgType
- | OpenConstrArgType
- | CastedOpenConstrArgType
+ | TacticArgType of int
+ | OpenConstrArgType of bool
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
@@ -268,4 +272,3 @@ val in_gen :
('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument
val out_gen :
('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a
-
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 0929119c..71bd431d 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: modintern.ml,v 1.2.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(* $Id: modintern.ml 6582 2005-01-13 14:28:56Z sacerdot $ *)
open Pp
open Util
@@ -79,10 +79,10 @@ let lookup_modtype (loc,qid) =
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
let transl_with_decl env = function
- | CWith_Module ((_,id),qid) ->
- With_Module (id,lookup_module qid)
- | CWith_Definition ((_,id),c) ->
- With_Definition (id,interp_constr Evd.empty env c)
+ | CWith_Module ((_,fqid),qid) ->
+ With_Module (fqid,lookup_module qid)
+ | CWith_Definition ((_,fqid),c) ->
+ With_Definition (fqid,interp_constr Evd.empty env c)
let rec interp_modtype env = function
| CMTEident qid ->
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 050d9f94..844450ac 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modintern.mli,v 1.1.6.1 2004/07/16 19:30:22 herbelin Exp $ i*)
+(*i $Id: modintern.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Declarations
diff --git a/interp/symbols.ml b/interp/notation.ml
index d1abb084..cb996dfe 100644
--- a/interp/symbols.ml
+++ b/interp/notation.ml
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *)
+(* $Id: notation.ml 7984 2006-02-04 20:14:55Z herbelin $ *)
(*i*)
open Util
open Pp
-open Bignat
+open Bigint
open Names
+open Term
open Nametab
open Libnames
open Summary
@@ -30,7 +31,7 @@ open Ppextend
terms and patterns can be set; these interpreters are in permanent table
[numeral_interpreter_tab]
- a set of ML printers for expressions denoting numbers parsable in
- this scope (permanently declared in [Esyntax.primitive_printer_tab])
+ this scope
- a set of interpretations for infix (more generally distfix) notations
- an optional pair of delimiters which, when occurring in a syntactic
expression, set this scope to be the current scope
@@ -41,20 +42,21 @@ open Ppextend
type level = precedence * tolerability list
type delimiters = string
+type notation_location = dir_path * string
type scope = {
- notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
+ notations: (string, interpretation * notation_location) Gmap.t;
delimiters: delimiters option
}
(* Uninterpreted notation map: notation -> level * dir_path *)
-let notation_level_map = ref Stringmap.empty
+let notation_level_map = ref Gmap.empty
(* Scopes table: scope_name -> symbol_interpretation *)
-let scope_map = ref Stringmap.empty
+let scope_map = ref Gmap.empty
let empty_scope = {
- notations = Stringmap.empty;
+ notations = Gmap.empty;
delimiters = None
}
@@ -62,20 +64,20 @@ let default_scope = "" (* empty name, not available from outside *)
let type_scope = "type_scope" (* special scope used for interpreting types *)
let init_scope_map () =
- scope_map := Stringmap.add default_scope empty_scope !scope_map;
- scope_map := Stringmap.add type_scope empty_scope !scope_map
+ scope_map := Gmap.add default_scope empty_scope !scope_map;
+ scope_map := Gmap.add type_scope empty_scope !scope_map
(**********************************************************************)
(* Operations on scopes *)
let declare_scope scope =
- try let _ = Stringmap.find scope !scope_map in ()
+ try let _ = Gmap.find scope !scope_map in ()
with Not_found ->
(* Options.if_verbose message ("Creating scope "^scope);*)
- scope_map := Stringmap.add scope empty_scope !scope_map
+ scope_map := Gmap.add scope empty_scope !scope_map
let find_scope scope =
- try Stringmap.find scope !scope_map
+ try Gmap.find scope !scope_map
with Not_found -> error ("Scope "^scope^" is not declared")
let check_scope sc = let _ = find_scope sc in ()
@@ -93,9 +95,14 @@ let current_scopes () = !scope_stack
(* TODO: push nat_scope, z_scope, ... in scopes summary *)
(* Exportation of scopes *)
-let cache_scope (_,(local,op,sc)) =
+let open_scope i (_,(local,op,sc)) =
+ if i=1 then begin
(match sc with Scope sc -> check_scope sc | _ -> ());
scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack
+ end
+
+let cache_scope o =
+ open_scope 1 o
let subst_scope (_,subst,sc) = sc
@@ -109,7 +116,7 @@ let export_scope (local,_,_ as x) = if local then None else Some x
let (inScope,outScope) =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
- open_function = (fun i o -> if i=1 then cache_scope o);
+ open_function = open_scope;
subst_function = subst_scope;
classify_function = classify_scope;
export_function = export_scope }
@@ -121,10 +128,12 @@ let empty_scope_stack = []
let push_scope sc scopes = Scope sc :: scopes
+let push_scopes = List.fold_right push_scope
+
(**********************************************************************)
(* Delimiters *)
-let delimiters_map = ref Stringmap.empty
+let delimiters_map = ref Gmap.empty
let declare_delimiters scope key =
let sc = find_scope scope in
@@ -134,15 +143,15 @@ let declare_delimiters scope key =
warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
end;
let sc = { sc with delimiters = Some key } in
- scope_map := Stringmap.add scope sc !scope_map;
- if Stringmap.mem key !delimiters_map then begin
- let oldsc = Stringmap.find key !delimiters_map in
+ scope_map := Gmap.add scope sc !scope_map;
+ if Gmap.mem key !delimiters_map then begin
+ let oldsc = Gmap.find key !delimiters_map in
Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
end;
- delimiters_map := Stringmap.add key scope !delimiters_map
+ delimiters_map := Gmap.add key scope !delimiters_map
let find_delimiters_scope loc key =
- try Stringmap.find key !delimiters_map
+ try Gmap.find key !delimiters_map
with Not_found ->
user_err_loc
(loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
@@ -162,7 +171,7 @@ type key =
(* Scopes table : interpretation -> scope_name *)
let notations_key_table = ref Gmapl.empty
-let numeral_key_table = Hashtbl.create 7
+let prim_token_key_table = Hashtbl.create 7
let rawconstr_key = function
| RApp (_,RRef (_,ref),_) -> RefKey ref
@@ -186,50 +195,66 @@ let pattern_key = function
(**********************************************************************)
(* Interpreting numbers (not in summary because functional objects) *)
-type num_interpreter =
- (loc -> bigint -> rawconstr)
- * (loc -> bigint -> name -> cases_pattern) option
+type required_module = section_path * string list
-type num_uninterpreter =
- rawconstr list * (rawconstr -> bigint option)
- * (cases_pattern -> bigint option) option
+type 'a prim_token_interpreter =
+ loc -> 'a -> rawconstr
-type required_module = global_reference * string list
+type cases_pattern_status = bool (* true = use prim token in patterns *)
-let numeral_interpreter_tab =
- (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t)
+type 'a prim_token_uninterpreter =
+ rawconstr list * (rawconstr -> 'a option) * cases_pattern_status
-let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
+type internal_prim_token_interpreter =
+ loc -> prim_token -> required_module * (unit -> rawconstr)
+
+let prim_token_interpreter_tab =
+ (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
+
+let add_prim_token_interpreter sc interp =
+ try
+ let cont = Hashtbl.find prim_token_interpreter_tab sc in
+ Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
+ with Not_found ->
+ let cont = (fun _loc _p -> raise Not_found) in
+ Hashtbl.add prim_token_interpreter_tab sc (interp cont)
+
+let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
declare_scope sc;
- Hashtbl.add numeral_interpreter_tab sc (dir,interp);
- List.iter
- (fun pat -> Hashtbl.add numeral_key_table (rawconstr_key pat)
- (sc,uninterp,uninterpc))
+ add_prim_token_interpreter sc interp;
+ List.iter (fun pat ->
+ Hashtbl.add prim_token_key_table (rawconstr_key pat) (sc,uninterp,b))
patl
-let check_required_module loc sc (ref,d) =
- let d' = List.map id_of_string d in
- let dir = make_dirpath (List.rev d') in
- try let _ = sp_of_global ref in ()
+let mkNumeral n = Numeral n
+let mkString s = String s
+
+let delay dir int loc x = (dir, (fun () -> int loc x))
+
+let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
+ declare_prim_token_interpreter sc
+ (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
+ (patl, (fun r -> option_app mkNumeral (uninterp r)), inpat)
+
+let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
+ declare_prim_token_interpreter sc
+ (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
+ (patl, (fun r -> option_app mkString (uninterp r)), inpat)
+
+let check_required_module loc sc (sp,d) =
+ try let _ = Nametab.absolute_reference sp in ()
with Not_found ->
- user_err_loc (loc,"numeral_interpreter",
- str ("Cannot interpret numbers in "^sc^" without requiring first module "
+ user_err_loc (loc,"prim_token_interpreter",
+ str ("Cannot interpret in "^sc^" without requiring first module "
^(list_last d)))
-let lookup_numeral_interpreter loc = function
- | Scope sc ->
- let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in
- check_required_module loc sc dir;
- interpreter
- | SingleNotation _ -> raise Not_found
-
(* Look if some notation or numeral printer in [scope] can be used in
the scope stack [scopes], and if yes, using delimiters or not *)
let find_with_delimiters = function
| None -> None
| Some scope ->
- match (Stringmap.find scope !scope_map).delimiters with
+ match (Gmap.find scope !scope_map).delimiters with
| Some key -> Some (Some scope, Some key)
| None -> None
@@ -257,48 +282,80 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
(* Uninterpreted notation levels *)
let declare_notation_level ntn level =
- if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
+ if Gmap.mem ntn !notation_level_map then
error ("Notation "^ntn^" is already assigned a level");
- notation_level_map := Stringmap.add ntn level !notation_level_map
+ notation_level_map := Gmap.add ntn level !notation_level_map
let level_of_notation ntn =
- Stringmap.find ntn !notation_level_map
+ Gmap.find ntn !notation_level_map
(* The mapping between notations and their interpretation *)
-let declare_notation_interpretation ntn scopt pat df pp8only =
+let declare_notation_interpretation ntn scopt pat df =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
- if Stringmap.mem ntn sc.notations && Options.is_verbose () then
+ if Gmap.mem ntn sc.notations && Options.is_verbose () then
warning ("Notation "^ntn^" was already used"^
(if scopt = None then "" else " in scope "^scope));
- let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
- scope_map := Stringmap.add scope sc !scope_map;
+ let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
+ scope_map := Gmap.add scope sc !scope_map;
if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
let declare_uninterpretation rule (metas,c as pat) =
let (key,n) = aconstr_key c in
notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
-let rec find_interpretation f = function
- | sce :: scopes ->
- let scope = match sce with
- | Scope s -> s
- | SingleNotation _ -> default_scope in
- (try f scope
- with Not_found -> find_interpretation f scopes)
+let rec find_interpretation find = function
| [] -> raise Not_found
+ | sce :: scopes ->
+ let sc,sco = match sce with
+ | Scope sc -> sc, Some sc
+ | SingleNotation _ -> default_scope, None in
+ try
+ let (pat,df) = find sc in
+ pat,(df,sco)
+ with Not_found ->
+ find_interpretation find scopes
+
+let find_notation ntn sc =
+ Gmap.find ntn (find_scope sc).notations
+
+let notation_of_prim_token = function
+ | Numeral n when is_pos_or_zero n -> to_string n
+ | Numeral n -> "- "^(to_string (neg n))
+ | String _ -> raise Not_found
+
+let find_prim_token g loc p sc =
+ (* Try for a user-defined numerical notation *)
+ try
+ let (_,c),df = find_notation (notation_of_prim_token p) sc in
+ g (rawconstr_of_aconstr loc c),df
+ with Not_found ->
+ (* Try for a primitive numerical notation *)
+ let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
+ check_required_module loc sc spdir;
+ g (interp ()), (dirpath (fst spdir),"")
+
+let interp_prim_token_gen g loc p scopes =
+ let all_scopes = push_scopes scopes !scope_stack in
+ try find_interpretation (find_prim_token g loc p) all_scopes
+ with Not_found ->
+ user_err_loc (loc,"interp_prim_token",
+ (match p with
+ | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
+ | String s -> str "No interpretation for string " ++ qs s))
+
+let interp_prim_token =
+ interp_prim_token_gen (fun x -> x)
+
+let interp_prim_token_cases_pattern loc p name =
+ interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p
let rec interp_notation loc ntn scopes =
- let f sc =
- let scope = find_scope sc in
- let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
- if pp8only then raise Not_found;
- pat,(df,if sc = default_scope then None else Some sc) in
- try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
- with Not_found ->
+ try find_interpretation (find_notation ntn) (push_scopes scopes !scope_stack)
+ with Not_found ->
user_err_loc
- (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
+ (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
let uninterp_notations c =
Gmapl.find (rawconstr_key c) !notations_key_table
@@ -308,47 +365,30 @@ let uninterp_cases_pattern_notations c =
let availability_of_notation (ntn_scope,ntn) scopes =
let f scope =
- Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
+ Gmap.mem ntn (Gmap.find scope !scope_map).notations in
find_without_delimiters f (ntn_scope,Some ntn) scopes
-let rec interp_numeral_gen loc f n = function
- | scope :: scopes ->
- (try f (lookup_numeral_interpreter loc scope)
- with Not_found -> interp_numeral_gen loc f n scopes)
- | [] ->
- user_err_loc (loc,"interp_numeral",
- str "No interpretation for numeral " ++ pr_bigint n)
-
-let interp_numeral loc n scopes =
- interp_numeral_gen loc (fun x -> fst x loc n) n
- (List.fold_right push_scope scopes !scope_stack)
-
-let interp_numeral_as_pattern loc n name scopes =
- let f x = match snd x with
- | None -> raise Not_found
- | Some g -> g loc n name in
- interp_numeral_gen loc f n (List.fold_right push_scope scopes !scope_stack)
-
-let uninterp_numeral c =
+let uninterp_prim_token c =
try
- let (sc,numpr,_) = Hashtbl.find numeral_key_table (rawconstr_key c) in
+ let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in
match numpr c with
| None -> raise No_match
| Some n -> (sc,n)
with Not_found -> raise No_match
-let uninterp_cases_numeral c =
+let uninterp_prim_token_cases_pattern c =
try
- match Hashtbl.find numeral_key_table (pattern_key c) with
- | (_,_,None) -> raise No_match
- | (sc,_,Some numpr) ->
- match numpr c with
- | None -> raise No_match
- | Some n -> (sc,n)
+ let k = cases_pattern_key c in
+ let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in
+ if not b then raise No_match;
+ let na,c = rawconstr_of_closed_cases_pattern c in
+ match numpr c with
+ | None -> raise No_match
+ | Some n -> (na,sc,n)
with Not_found -> raise No_match
-let availability_of_numeral printer_scope scopes =
- let f scope = Hashtbl.mem numeral_interpreter_tab scope in
+let availability_of_prim_token printer_scope scopes =
+ let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
(* Miscellaneous *)
@@ -356,35 +396,10 @@ let availability_of_numeral printer_scope scopes =
let exists_notation_in_scope scopt ntn r =
let scope = match scopt with Some s -> s | None -> default_scope in
try
- let sc = Stringmap.find scope !scope_map in
- let (r',_,pp8only) = Stringmap.find ntn sc.notations in
- r' = r, pp8only
- with Not_found -> false, false
-
-(* Special scopes associated to arguments of a global reference *)
-
-let arguments_scope = ref Refmap.empty
-
-let cache_arguments_scope (_,(r,scl)) =
- List.iter (option_iter check_scope) scl;
- arguments_scope := Refmap.add r scl !arguments_scope
-
-let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl)
-
-let (inArgumentsScope,outArgumentsScope) =
- declare_object {(default_object "ARGUMENTS-SCOPE") with
- cache_function = cache_arguments_scope;
- load_function = (fun _ o -> cache_arguments_scope o);
- subst_function = subst_arguments_scope;
- classify_function = (fun (_,o) -> Substitute o);
- export_function = (fun x -> Some x) }
-
-let declare_arguments_scope r scl =
- Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
-
-let find_arguments_scope r =
- try Refmap.find r !arguments_scope
- with Not_found -> []
+ let sc = Gmap.find scope !scope_map in
+ let (r',_) = Gmap.find ntn sc.notations in
+ r' = r
+ with Not_found -> false
(**********************************************************************)
(* Mapping classes to scopes *)
@@ -401,8 +416,6 @@ let declare_class_scope sc cl =
let find_class_scope cl =
Gmap.find cl !class_scope_map
-open Term
-
let find_class t =
let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in
match kind_of_term t with
@@ -413,6 +426,9 @@ let find_class t =
| Sort _ -> CL_SORT
| _ -> raise Not_found
+(**********************************************************************)
+(* Special scopes associated to arguments of a global reference *)
+
let rec compute_arguments_scope t =
match kind_of_term (Reductionops.whd_betaiotazeta t) with
| Prod (_,t,u) ->
@@ -421,6 +437,37 @@ let rec compute_arguments_scope t =
sc :: compute_arguments_scope u
| _ -> []
+let arguments_scope = ref Refmap.empty
+
+let load_arguments_scope _ (_,(r,scl)) =
+ List.iter (option_iter check_scope) scl;
+ arguments_scope := Refmap.add r scl !arguments_scope
+
+let cache_arguments_scope o =
+ load_arguments_scope 1 o
+
+let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl)
+
+let discharge_arguments_scope (r,_) =
+ match r with
+ | VarRef _ -> None
+ | _ -> Some (r,compute_arguments_scope (Global.type_of_global r))
+
+let (inArgumentsScope,outArgumentsScope) =
+ declare_object {(default_object "ARGUMENTS-SCOPE") with
+ cache_function = cache_arguments_scope;
+ load_function = load_arguments_scope;
+ subst_function = subst_arguments_scope;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x) }
+
+let declare_arguments_scope r scl =
+ Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
+
+let find_arguments_scope r =
+ try Refmap.find r !arguments_scope
+ with Not_found -> []
+
let declare_ref_arguments_scope ref =
let t = Global.type_of_global ref in
declare_arguments_scope ref (compute_arguments_scope t)
@@ -478,36 +525,33 @@ let pr_scope_classes sc =
hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
spc() ++ prlist_with_sep spc pr_class l) ++ fnl()
-let rec rawconstr_of_aconstr () x =
- rawconstr_of_aconstr_with_binders dummy_loc (fun id () -> (id,()))
- rawconstr_of_aconstr () x
-
let pr_notation_info prraw ntn c =
- str "\"" ++ str ntn ++ str "\" := " ++ prraw (rawconstr_of_aconstr () c)
+ str "\"" ++ str ntn ++ str "\" := " ++
+ prraw (rawconstr_of_aconstr dummy_loc c)
let pr_named_scope prraw scope sc =
(if scope = default_scope then
- match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
+ match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
| 0 -> str "No lonely notation"
| n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
else
str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
++ fnl ()
++ pr_scope_classes scope
- ++ Stringmap.fold
- (fun ntn ((_,r),(_,df),_) strm ->
+ ++ Gmap.fold
+ (fun ntn ((_,r),(_,df)) strm ->
pr_notation_info prraw df r ++ fnl () ++ strm)
sc.notations (mt ())
let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
let pr_scopes prraw =
- Stringmap.fold
+ Gmap.fold
(fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
!scope_map (mt ())
let rec find_default ntn = function
- | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
+ | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations ->
Some scope
| SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
| _::scopes -> find_default ntn scopes
@@ -531,9 +575,9 @@ let browse_notation ntn map =
if String.contains ntn ' ' then (=) ntn
else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
let l =
- Stringmap.fold
+ Gmap.fold
(fun scope_name sc ->
- Stringmap.fold (fun ntn ((_,r),df,_) l ->
+ Gmap.fold (fun ntn ((_,r),df) l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
map [] in
let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
@@ -560,8 +604,8 @@ let locate_notation prraw ntn =
let collect_notation_in_scope scope sc known =
assert (scope <> default_scope);
- Stringmap.fold
- (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
+ Gmap.fold
+ (fun ntn ((_,r),(_,df)) (l,known as acc) ->
if List.mem ntn known then acc else ((df,r)::l,ntn::known))
sc.notations ([],known)
@@ -577,8 +621,8 @@ let collect_notations stack =
| SingleNotation ntn ->
if List.mem ntn knownntn then (all,knownntn)
else
- let ((_,r),(_,df),_) =
- Stringmap.find ntn (find_scope default_scope).notations in
+ let ((_,r),(_,df)) =
+ Gmap.find ntn (find_scope default_scope).notations in
let all' = match all with
| (s,lonelyntn)::rest when s = default_scope ->
(s,(df,r)::lonelyntn)::rest
@@ -614,13 +658,13 @@ type unparsing_rule = unparsing list * precedence
(* Concrete syntax for symbolic-extension table *)
let printing_rules =
- ref (Stringmap.empty : unparsing_rule Stringmap.t)
+ ref (Gmap.empty : (string,unparsing_rule) Gmap.t)
let declare_notation_printing_rule ntn unpl =
- printing_rules := Stringmap.add ntn unpl !printing_rules
+ printing_rules := Gmap.add ntn unpl !printing_rules
let find_notation_printing_rule ntn =
- try Stringmap.find ntn !printing_rules
+ try Gmap.find ntn !printing_rules
with Not_found -> anomaly ("No printing rule found for "^ntn)
(**********************************************************************)
@@ -644,13 +688,13 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
let init () =
init_scope_map ();
(*
- scope_stack := Stringmap.empty
+ scope_stack := Gmap.empty
arguments_scope := Refmap.empty
*)
- notation_level_map := Stringmap.empty;
- delimiters_map := Stringmap.empty;
+ notation_level_map := Gmap.empty;
+ delimiters_map := Gmap.empty;
notations_key_table := Gmapl.empty;
- printing_rules := Stringmap.empty;
+ printing_rules := Gmap.empty;
class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
let _ =
diff --git a/interp/symbols.mli b/interp/notation.mli
index 5401ae77..32ec7a96 100644
--- a/interp/symbols.mli
+++ b/interp/notation.mli
@@ -6,12 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: symbols.mli,v 1.22.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: notation.mli 7984 2006-02-04 20:14:55Z herbelin $ i*)
(*i*)
open Util
open Pp
-open Bignat
+open Bigint
open Names
open Nametab
open Libnames
@@ -50,36 +50,47 @@ val push_scope : scope_name -> scopes -> scopes
val declare_delimiters : scope_name -> delimiters -> unit
val find_delimiters_scope : loc -> delimiters -> scope_name
-(*s Declare and uses back and forth a numeral interpretation *)
+(*s Declare and uses back and forth an interpretation of primitive token *)
(* A numeral interpreter is the pair of an interpreter for **integer**
numbers in terms and an optional interpreter in pattern, if
negative numbers are not supported, the interpreter must fail with
an appropriate error message *)
-type num_interpreter =
- (loc -> bigint -> rawconstr)
- * (loc -> bigint -> name -> cases_pattern) option
+type notation_location = dir_path * string
+type required_module = section_path * string list
+type cases_pattern_status = bool (* true = use prim token in patterns *)
-type num_uninterpreter =
- rawconstr list * (rawconstr -> bigint option)
- * (cases_pattern -> bigint option) option
+type 'a prim_token_interpreter =
+ loc -> 'a -> rawconstr
+
+type 'a prim_token_uninterpreter =
+ rawconstr list * (rawconstr -> 'a option) * cases_pattern_status
-type required_module = global_reference * string list
val declare_numeral_interpreter : scope_name -> required_module ->
- num_interpreter -> num_uninterpreter -> unit
+ bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit
+
+val declare_string_interpreter : scope_name -> required_module ->
+ string prim_token_interpreter -> string prim_token_uninterpreter -> unit
+
+(* Return the [term]/[cases_pattern] bound to a primitive token in a
+ given scope context*)
-(* Return the [term]/[cases_pattern] bound to a numeral in a given scope context*)
-val interp_numeral : loc -> bigint -> scope_name list -> rawconstr
-val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list ->
- cases_pattern
+val interp_prim_token : loc -> prim_token -> scope_name list ->
+ rawconstr * (notation_location * scope_name option)
+val interp_prim_token_cases_pattern : loc -> prim_token -> name ->
+ scope_name list -> cases_pattern * (notation_location * scope_name option)
-(* Return the numeral bound to a [term]/[cases_pattern]; raise [No_match] if no *)
-(* such numeral *)
-val uninterp_numeral : rawconstr -> scope_name * bigint
-val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
+(* Return the primitive token associated to a [term]/[cases_pattern];
+ raise [No_match] if no such token *)
-val availability_of_numeral : scope_name -> scopes -> delimiters option option
+val uninterp_prim_token :
+ rawconstr -> scope_name * prim_token
+val uninterp_prim_token_cases_pattern :
+ cases_pattern -> name * scope_name * prim_token
+
+val availability_of_prim_token :
+ scope_name -> scopes -> delimiters option option
(*s Declare and interpret back and forth a notation *)
@@ -87,14 +98,15 @@ val availability_of_numeral : scope_name -> scopes -> delimiters option option
type interp_rule =
| NotationRule of scope_name option * notation
| SynDefRule of kernel_name
+
val declare_notation_interpretation : notation -> scope_name option ->
- interpretation -> dir_path * string -> bool -> unit
+ interpretation -> notation_location -> unit
val declare_uninterpretation : interp_rule -> interpretation -> unit
(* Return the interpretation bound to a notation *)
val interp_notation : loc -> notation -> scope_name list ->
- interpretation * ((dir_path * string) * scope_name option)
+ interpretation * (notation_location * scope_name option)
(* Return the possible notations for a given term *)
val uninterp_notations : rawconstr ->
@@ -103,23 +115,21 @@ val uninterp_cases_pattern_notations : cases_pattern ->
(interp_rule * interpretation * int option) list
(* Test if a notation is available in the scopes *)
-(* context [scopes] if available, the result is not None; the first *)
-(* argument is itself not None if a delimiters is needed; the second *)
-(* argument is a numeral printer if the *)
+(* context [scopes]; if available, the result is not None; the first *)
+(* argument is itself not None if a delimiters is needed *)
val availability_of_notation : scope_name option * notation -> scopes ->
(scope_name option * delimiters option) option
(*s Declare and test the level of a (possibly uninterpreted) notation *)
-val declare_notation_level : notation -> level option * level -> unit
-val level_of_notation : notation -> level option * level
- (* raise [Not_found] if no level *)
+val declare_notation_level : notation -> level -> unit
+val level_of_notation : notation -> level (* raise [Not_found] if no level *)
(*s** Miscellaneous *)
(* Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
- interpretation -> bool * bool
+ interpretation -> bool
(* Declares and looks for scopes associated to arguments of a global ref *)
val declare_arguments_scope: global_reference -> scope_name option list -> unit
@@ -157,4 +167,4 @@ val declare_notation_printing_rule : notation -> unparsing_rule -> unit
val find_notation_printing_rule : notation -> unparsing_rule
(**********************************************************************)
-(* Rem: printing rules for numerals are trivial *)
+(* Rem: printing rules for primitive token are canonical *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 29fb7cc7..34e93624 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppextend.ml,v 1.4.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(*i $Id: ppextend.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
(*i*)
open Pp
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index bc0a83ec..3d49c210 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppextend.mli,v 1.4.2.2 2005/01/21 16:41:50 herbelin Exp $ i*)
+(*i $Id: ppextend.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
(*i*)
open Pp
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 72899676..476fd7e6 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.ml,v 1.10.2.1 2004/07/16 19:30:22 herbelin Exp $ i*)
+(*i $Id: reserve.ml 7732 2005-12-26 13:51:24Z herbelin $ i*)
(* Reserved names *)
@@ -57,14 +57,11 @@ let rec unloc = function
| RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c)
| RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c)
| RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
- | RCases (_,(tyopt,rtntypopt),tml,pl) ->
+ | RCases (_,rtntypopt,tml,pl) ->
RCases (dummy_loc,
- (option_app unloc tyopt,ref (option_app unloc !rtntypopt)),
+ (option_app unloc rtntypopt),
List.map (fun (tm,x) -> (unloc tm,x)) tml,
List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
- | ROrderedCase (_,b,tyopt,tm,bv,x) ->
- ROrderedCase
- (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x)
| RLetTuple (_,nal,(na,po),b,c) ->
RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
| RIf (_,c,(na,po),b1,b2) ->
@@ -76,7 +73,7 @@ let rec unloc = function
bl,
Array.map unloc tyl,
Array.map unloc bv)
- | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)
+ | RCast (_,c,k,t) -> RCast (dummy_loc,unloc c,k,unloc t)
| RSort (_,x) -> RSort (dummy_loc,x)
| RHole (_,x) -> RHole (dummy_loc,x)
| RRef (_,x) -> RRef (dummy_loc,x)
@@ -86,10 +83,9 @@ let rec unloc = function
let anonymize_if_reserved na t = match na with
| Name id as na ->
- if !Options.v7 & id = id_of_string "_" then t else
(try
if unloc t = find_reserved_type id
- then RHole (dummy_loc,BinderType na)
+ then RHole (dummy_loc,Evd.BinderType na)
else t
with Not_found -> t)
| Anonymous -> t
diff --git a/interp/reserve.mli b/interp/reserve.mli
index a79e2c25..13349ee9 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.mli,v 1.2.2.1 2004/07/16 19:30:22 herbelin Exp $ i*)
+(*i $Id: reserve.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
open Util
open Names
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index ceda2b47..3389cd8a 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: syntax_def.ml,v 1.6.2.2 2006/01/03 20:33:31 herbelin Exp $ *)
+(* $Id: syntax_def.ml 7779 2006-01-03 20:33:47Z herbelin $ *)
open Util
open Pp
@@ -39,21 +39,21 @@ let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
add_syntax_constant kn c;
Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
if not onlyparse then
- (* Declare it to be used as (long) name *)
- Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
+ (* Declare it to be used as long name *)
+ Notation.declare_uninterpretation (Notation.SynDefRule kn) ([],c)
let open_syntax_constant i ((sp,kn),(_,c,onlyparse)) =
Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
if not onlyparse then
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared inbetween *)
- Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
+ Notation.declare_uninterpretation (Notation.SynDefRule kn) ([],c)
let cache_syntax_constant d =
load_syntax_constant 1 d
let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) =
- (local,subst_aconstr subst c,onlyparse)
+ (local,subst_aconstr subst [] c,onlyparse)
let classify_syntax_constant (_,(local,_,_ as o)) =
if local then Dispose else Substitute o
@@ -78,3 +78,15 @@ let rec set_loc loc _ a =
let search_syntactic_definition loc kn =
set_loc loc () (KNmap.find kn !syntax_table)
+
+exception BoundToASyntacticDefThatIsNotARef
+
+let locate_global qid =
+ match Nametab.extended_locate qid with
+ | TrueGlobal ref -> ref
+ | SyntacticDef kn ->
+ match search_syntactic_definition dummy_loc kn with
+ | Rawterm.RRef (_,ref) -> ref
+ | _ ->
+ errorlabstrm "" (pr_qualid qid ++
+ str " is bound to a notation that does not denote a reference")
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 0aec03c2..ac7318b5 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: syntax_def.mli,v 1.3.2.2 2004/07/16 19:30:23 herbelin Exp $ i*)
+(*i $Id: syntax_def.mli 7051 2005-05-20 15:45:51Z herbelin $ i*)
(*i*)
open Util
@@ -23,3 +23,10 @@ val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
val search_syntactic_definition : loc -> kernel_name -> rawconstr
+(* [locate_global] locates global reference possibly following a chain of
+ syntactic aliases; raise Not_found if not bound in the global env;
+ raise an error if bound to a syntactic def that does not denote a
+ reference *)
+
+val locate_global : Libnames.qualid -> Libnames.global_reference
+
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a2b6e8b7..82f74f40 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml,v 1.35.2.3 2004/11/17 09:51:41 herbelin Exp $ *)
+(* $Id: topconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
(*i*)
open Pp
@@ -16,6 +16,7 @@ open Nameops
open Libnames
open Rawterm
open Term
+open Mod_subst
(*i*)
(**********************************************************************)
@@ -36,20 +37,19 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option * aconstr option *
+ | ACases of aconstr option *
(aconstr * (name * (inductive * name list) option)) list *
(identifier list * cases_pattern list * aconstr) list
- | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ASort of rawsort
- | AHole of hole_kind
+ | AHole of Evd.hole_kind
| APatVar of patvar
- | ACast of aconstr * aconstr
+ | ACast of aconstr * cast_kind * aconstr
let name_app f e = function
- | Name id -> let (id, e) = f id e in (Name id, e)
- | Anonymous -> Anonymous, e
+ | Name id -> let (id, e) = f id e in (e, Name id)
+ | Anonymous -> e,Anonymous
let rec subst_rawvars l = function
| RVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
@@ -67,40 +67,44 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
subst_rawvars outerl it
| ALambda (na,ty,c) ->
- let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
+ let e,na = name_app g e na in RLambda (loc,na,f e ty,f e c)
| AProd (na,ty,c) ->
- let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
+ let e,na = name_app g e na in RProd (loc,na,f e ty,f e c)
| ALetIn (na,b,c) ->
- let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
- | ACases (tyopt,rtntypopt,tml,eqnl) ->
- let cases_predicate_names tml =
- List.flatten (List.map (function
- | (tm,(na,None)) -> [na]
- | (tm,(na,Some (_,nal))) -> na::nal) tml) in
- (* TODO: apply g to na (in fact not used) *)
- let e' = List.fold_right
- (fun na e -> snd (name_app g e na)) (cases_predicate_names tml) e in
+ let e,na = name_app g e na in RLetIn (loc,na,f e b,f e c)
+ | ACases (rtntypopt,tml,eqnl) ->
+ let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
+ let e',t' = match t with
+ | None -> e',None
+ | Some (ind,nal) ->
+ let e',nal' = List.fold_right (fun na (e',nal) ->
+ let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in
+ e',Some (loc,ind,nal') in
+ let e',na' = name_app g e' na in
+ (e',(f e tm,(na',t'))::tml')) tml (e,[]) in
let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
- let eqnl = List.map (fun (idl,pat,rhs) ->
- let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in
- RCases (loc,(option_app (f e) tyopt, ref (option_app (f e') rtntypopt)),
- List.map (fun (tm,(na,x)) ->
- (f e tm,ref (na,option_app (fun (x,y) -> (loc,x,y)) x))) tml,eqnl)
- | AOrderedCase (b,tyopt,tm,bv) ->
- ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv,ref None)
+ let eqnl' = List.map (fun (idl,pat,rhs) ->
+ let (idl,e) = List.fold_right fold idl ([],e) in
+ (loc,idl,pat,f e rhs)) eqnl in
+ RCases (loc,option_app (f e') rtntypopt,tml',eqnl')
| ALetTuple (nal,(na,po),b,c) ->
- let e,nal = list_fold_map (fun e na -> let (na,e) = name_app g e na in e,na) e nal in
- let na,e = name_app g e na in
+ let e,nal = list_fold_map (name_app g) e nal in
+ let e,na = name_app g e na in
RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
| AIf (c,(na,po),b1,b2) ->
- let na,e = name_app g e na in
+ let e,na = name_app g e na in
RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2)
- | ACast (c,t) -> RCast (loc,f e c,f e t)
+ | ACast (c,k,t) -> RCast (loc,f e c,k,f e t)
| ASort x -> RSort (loc,x)
| AHole x -> RHole (loc,x)
| APatVar n -> RPatVar (loc,(false,n))
| ARef x -> RRef (loc,x)
+let rec rawconstr_of_aconstr loc x =
+ let rec aux () x =
+ rawconstr_of_aconstr_with_binders loc (fun id () -> (id,())) aux () x
+ in aux () x
+
let rec subst_pat subst pat =
match pat with
| PatVar _ -> pat
@@ -110,100 +114,6 @@ let rec subst_pat subst pat =
if kn' == kn && cpl' == cpl then pat else
PatCstr (loc,((kn',i),j),cpl',n)
-let rec subst_aconstr subst raw =
- match raw with
- | ARef ref ->
- let ref' = subst_global subst ref in
- if ref' == ref then raw else
- ARef ref'
-
- | AVar _ -> raw
-
- | AApp (r,rl) ->
- let r' = subst_aconstr subst r
- and rl' = list_smartmap (subst_aconstr subst) rl in
- if r' == r && rl' == rl then raw else
- AApp(r',rl')
-
- | AList (id1,id2,r1,r2,b) ->
- let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
- if r1' == r1 && r2' == r2 then raw else
- AList (id1,id2,r1',r2',b)
-
- | ALambda (n,r1,r2) ->
- let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
- if r1' == r1 && r2' == r2 then raw else
- ALambda (n,r1',r2')
-
- | AProd (n,r1,r2) ->
- let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
- if r1' == r1 && r2' == r2 then raw else
- AProd (n,r1',r2')
-
- | ALetIn (n,r1,r2) ->
- let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
- if r1' == r1 && r2' == r2 then raw else
- ALetIn (n,r1',r2')
-
- | ACases (ro,rtntypopt,rl,branches) ->
- let ro' = option_smartmap (subst_aconstr subst) ro
- and rtntypopt' = option_smartmap (subst_aconstr subst) rtntypopt
- and rl' = list_smartmap
- (fun (a,(n,signopt) as x) ->
- let a' = subst_aconstr subst a in
- let signopt' = option_app (fun ((indkn,i),nal as z) ->
- let indkn' = subst_kn subst indkn in
- if indkn == indkn' then z else ((indkn',i),nal)) signopt in
- if a' == a && signopt' == signopt then x else (a',(n,signopt')))
- rl
- and branches' = list_smartmap
- (fun (idl,cpl,r as branch) ->
- let cpl' = list_smartmap (subst_pat subst) cpl
- and r' = subst_aconstr subst r in
- if cpl' == cpl && r' == r then branch else
- (idl,cpl',r'))
- branches
- in
- if ro' == ro && rtntypopt == rtntypopt' &
- rl' == rl && branches' == branches then raw else
- ACases (ro',rtntypopt',rl',branches')
-
- | AOrderedCase (b,ro,r,ra) ->
- let ro' = option_smartmap (subst_aconstr subst) ro
- and r' = subst_aconstr subst r
- and ra' = array_smartmap (subst_aconstr subst) ra in
- if ro' == ro && r' == r && ra' == ra then raw else
- AOrderedCase (b,ro',r',ra')
-
- | ALetTuple (nal,(na,po),b,c) ->
- let po' = option_smartmap (subst_aconstr subst) po
- and b' = subst_aconstr subst b
- and c' = subst_aconstr subst c in
- if po' == po && b' == b && c' == c then raw else
- ALetTuple (nal,(na,po'),b',c')
-
- | AIf (c,(na,po),b1,b2) ->
- let po' = option_smartmap (subst_aconstr subst) po
- and b1' = subst_aconstr subst b1
- and b2' = subst_aconstr subst b2
- and c' = subst_aconstr subst c in
- if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
- AIf (c',(na,po'),b1',b2')
-
- | APatVar _ | ASort _ -> raw
-
- | AHole (ImplicitArg (ref,i)) ->
- let ref' = subst_global subst ref in
- if ref' == ref then raw else
- AHole (ImplicitArg (ref',i))
- | AHole (BinderType _ | QuestionMark | CasesType |
- InternalHole | TomatchTypeParameter _) -> raw
-
- | ACast (r1,r2) ->
- let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
- if r1' == r1 && r2' == r2 then raw else
- ACast (r1',r2')
-
let add_name r = function
| Anonymous -> ()
| Name id -> r := id :: !r
@@ -222,9 +132,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
f ty1 ty2 & f c1 c2
| RHole _, RHole _ -> true
| RSort (_,s1), RSort (_,s2) -> s1 = s2
- | (RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+ | (RLetIn _ | RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
- | _,(RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+ | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
-> error "Unsupported construction in recursive notations"
| (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
@@ -232,7 +142,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2
-let discriminate_patterns nl l1 l2 =
+let discriminate_patterns foundvars nl l1 l2 =
let diff = ref None in
let rec aux n c1 c2 = match c1,c2 with
| RVar (_,v1), RVar (_,v2) when v1<>v2 ->
@@ -245,42 +155,48 @@ let discriminate_patterns nl l1 l2 =
let l = list_map2_i aux 0 l1 l2 in
if not (List.for_all ((=) true) l) then
error "Both ends of the recursive pattern differ";
- !diff
+ match !diff with
+ | None -> error "Both ends of the recursive pattern are the same"
+ | Some (x,y,_ as discr) ->
+ List.iter (fun id ->
+ if List.mem id !foundvars
+ then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
+ foundvars := id::!foundvars) [x;y];
+ discr
let aconstr_and_vars_of_rawconstr a =
let found = ref [] in
- let bound_binders = ref [] in
let rec aux = function
- | RVar (_,id) ->
- if not (List.mem id !bound_binders) then found := id::!found;
- AVar id
+ | RVar (_,id) -> found := id::!found; AVar id
| RApp (_,f,args) when has_ldots args -> make_aconstr_list f args
+ | RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var ->
+ (* Special case for alternative (recursive) notation of application *)
+ let x,y,lassoc = discriminate_patterns found 0 [c] [d] in
+ found := ldots_var :: !found; assert lassoc;
+ AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc)
| RApp (_,g,args) -> AApp (aux g, List.map aux args)
- | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
- | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
- | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
- | RCases (_,(tyopt,rtntypopt),tml,eqnl) ->
+ | RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
+ | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
+ | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
+ | RCases (_,rtntypopt,tml,eqnl) ->
let f (_,idl,pat,rhs) =
- bound_binders := idl@(!bound_binders);
+ found := idl@(!found);
(idl,pat,aux rhs) in
- ACases (option_app aux tyopt,
- option_app aux !rtntypopt,
- List.map (fun (tm,{contents = (na,x)}) ->
- add_name bound_binders na;
+ ACases (option_app aux rtntypopt,
+ List.map (fun (tm,(na,x)) ->
+ add_name found na;
option_iter
- (fun (_,_,nl) -> List.iter (add_name bound_binders) nl) x;
+ (fun (_,_,nl) -> List.iter (add_name found) nl) x;
(aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
List.map f eqnl)
- | ROrderedCase (_,b,tyopt,tm,bv,_) ->
- AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
| RLetTuple (loc,nal,(na,po),b,c) ->
- add_name bound_binders na;
- List.iter (add_name bound_binders) nal;
+ add_name found na;
+ List.iter (add_name found) nal;
ALetTuple (nal,(na,option_app aux po),aux b,aux c)
| RIf (loc,c,(na,po),b1,b2) ->
- add_name bound_binders na;
+ add_name found na;
AIf (aux c,(na,option_app aux po),aux b1,aux b2)
- | RCast (_,c,t) -> ACast (aux c,aux t)
+ | RCast (_,c,k,t) -> ACast (aux c,k,aux t)
| RSort (_,s) -> ASort s
| RHole (_,w) -> AHole w
| RRef (_,r) -> ARef r
@@ -300,13 +216,7 @@ allowed in abbreviatable expressions"
error "Both ends of the recursive pattern have different lengths";
let ll2,l2' = list_chop nl l2 in
let t = List.hd l2' and lr2 = List.tl l2' in
- let discr = discriminate_patterns nl (ll1@lr1) (ll2@lr2) in
- let x,y,order = match discr with Some z -> z | None ->
- error "Both ends of the recursive pattern are the same" in
- List.iter (fun id ->
- if List.mem id !bound_binders or List.mem id !found
- then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
- found := id::!found) [x;y];
+ let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in
let iter =
if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
@@ -326,20 +236,126 @@ allowed in abbreviatable expressions"
in
let t = aux a in
(* Side effect *)
- t, !found, !bound_binders
+ t, !found
let aconstr_of_rawconstr vars a =
- let a,notbindingvars,binders = aconstr_and_vars_of_rawconstr a in
+ let a,foundvars = aconstr_and_vars_of_rawconstr a in
let check_type x =
- if not (List.mem x notbindingvars or List.mem x binders) then
+ if not (List.mem x foundvars) then
error ((string_of_id x)^" is unbound in the right-hand-side") in
List.iter check_type vars;
a
+let aconstr_of_constr avoiding t =
+ aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
+
+let rec subst_aconstr subst bound raw =
+ match raw with
+ | ARef ref ->
+ let ref',t = subst_global subst ref in
+ if ref' == ref then raw else
+ aconstr_of_constr bound t
+
+ | AVar _ -> raw
+
+ | AApp (r,rl) ->
+ let r' = subst_aconstr subst bound r
+ and rl' = list_smartmap (subst_aconstr subst bound) rl in
+ if r' == r && rl' == rl then raw else
+ AApp(r',rl')
+
+ | AList (id1,id2,r1,r2,b) ->
+ let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ AList (id1,id2,r1',r2',b)
+
+ | ALambda (n,r1,r2) ->
+ let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ ALambda (n,r1',r2')
+
+ | AProd (n,r1,r2) ->
+ let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ AProd (n,r1',r2')
+
+ | ALetIn (n,r1,r2) ->
+ let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ ALetIn (n,r1',r2')
+
+ | ACases (rtntypopt,rl,branches) ->
+ let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+ and rl' = list_smartmap
+ (fun (a,(n,signopt) as x) ->
+ let a' = subst_aconstr subst bound a in
+ let signopt' = option_app (fun ((indkn,i),nal as z) ->
+ let indkn' = subst_kn subst indkn in
+ if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+ if a' == a && signopt' == signopt then x else (a',(n,signopt')))
+ rl
+ and branches' = list_smartmap
+ (fun (idl,cpl,r as branch) ->
+ let cpl' = list_smartmap (subst_pat subst) cpl
+ and r' = subst_aconstr subst bound r in
+ if cpl' == cpl && r' == r then branch else
+ (idl,cpl',r'))
+ branches
+ in
+ if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
+ rl' == rl && branches' == branches then raw else
+ ACases (rtntypopt',rl',branches')
+
+ | ALetTuple (nal,(na,po),b,c) ->
+ let po' = option_smartmap (subst_aconstr subst bound) po
+ and b' = subst_aconstr subst bound b
+ and c' = subst_aconstr subst bound c in
+ if po' == po && b' == b && c' == c then raw else
+ ALetTuple (nal,(na,po'),b',c')
+
+ | AIf (c,(na,po),b1,b2) ->
+ let po' = option_smartmap (subst_aconstr subst bound) po
+ and b1' = subst_aconstr subst bound b1
+ and b2' = subst_aconstr subst bound b2
+ and c' = subst_aconstr subst bound c in
+ if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
+ AIf (c',(na,po'),b1',b2')
+
+ | APatVar _ | ASort _ -> raw
+
+ | AHole (Evd.ImplicitArg (ref,i)) ->
+ let ref',t = subst_global subst ref in
+ if ref' == ref then raw else
+ AHole (Evd.InternalHole)
+ | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType |
+ Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+
+ | ACast (r1,k,r2) ->
+ let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ ACast (r1',k,r2')
+
+
let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
(* Pattern-matching rawconstr and aconstr *)
+let abstract_return_type_context pi mklam tml rtno =
+ option_app (fun rtn ->
+ let nal =
+ List.flatten (List.map (fun (_,(na,t)) ->
+ match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
+ List.fold_right mklam nal rtn)
+ rtno
+
+let abstract_return_type_context_rawconstr =
+ abstract_return_type_context pi3
+ (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
+
+let abstract_return_type_context_aconstr =
+ abstract_return_type_context snd
+ (fun na c -> ALambda(na,AHole Evd.InternalHole,c))
+
let rec adjust_scopes = function
| _,[] -> []
| [],a::args -> (None,a) :: adjust_scopes ([],args)
@@ -366,6 +382,18 @@ let bind_env alp sigma var v =
(* TODO: handle the case of multiple occs in different scopes *)
(var,v)::sigma
+let match_opt f sigma t1 t2 = match (t1,t2) with
+ | None, None -> sigma
+ | Some t1, Some t2 -> f sigma t1 t2
+ | _ -> raise No_match
+
+let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
+ | (Name id1,Name id2) when List.mem id2 metas ->
+ alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
+ | (Name id1,Name id2) -> (id1,id2)::alp,sigma
+ | (Anonymous,Anonymous) -> alp,sigma
+ | _ -> raise No_match
+
let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
| RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
@@ -377,28 +405,34 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
when List.length l1 = List.length l2 ->
match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
| RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
- match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+ match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
| RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
- match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+ match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
| RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
- match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
- | RCases (_,(po1,rtno1),tml1,eqnl1), ACases (po2,rtno2,tml2,eqnl2)
+ match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
+ | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2)
when List.length tml1 = List.length tml2 ->
- let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
- (* TODO: match rtno' with their contexts *)
- let sigma = List.fold_left2
+ let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
+ let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
+ let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
+ let sigma = List.fold_left2
(fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
- List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
- | ROrderedCase (_,st,po1,c1,bl1,_), AOrderedCase (st2,po2,c2,bl2)
- when Array.length bl1 = Array.length bl2 ->
- let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
- array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2
- | RCast(_,c1,t1), ACast(c2,t2) ->
+ List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
+ | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
+ let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
+ List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
+ | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2)
+ when List.length nal1 = List.length nal2 ->
+ let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
+ let sigma = match_ alp metas sigma b1 b2 in
+ let (alp,sigma) =
+ List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
+ match_ alp metas sigma c1 c2
+ | RCast(_,c1,_,t1), ACast(c2,_,t2) ->
match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
| RSort (_,s1), ASort s2 when s1 = s2 -> sigma
| RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
- | a, AHole _ when not(Options.do_translate()) -> sigma
- | RHole _, AHole _ -> sigma
+ | a, AHole _ -> sigma
| (RDynamic _ | RRec _ | REvar _), _
| _,_ -> raise No_match
@@ -423,13 +457,9 @@ and match_alist alp metas sigma l1 l2 x iter termin lassoc =
let tl,sigma = match_alist_tail alp metas sigma [t1] rest in
(x,encode_list_value (if lassoc then List.rev tl else tl))::sigma
-and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
- | (Name id1,Name id2) when List.mem id2 metas ->
- let sigma = bind_env alp sigma id2 (RVar (dummy_loc,id1)) in
- match_ alp metas sigma b1 b2
- | (Name id1,Name id2) -> match_ ((id1,id2)::alp) metas sigma b1 b2
- | (Anonymous,Anonymous) -> match_ alp metas sigma b1 b2
- | _ -> raise No_match
+and match_binders alp metas na1 na2 sigma b1 b2 =
+ let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
+ match_ alp metas sigma b1 b2
and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
@@ -461,12 +491,15 @@ type explicitation = ExplByPos of int | ExplByName of identifier
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
+type prim_token = Numeral of Bigint.bigint | String of string
+
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
+ | CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr list
- | CPatNumeral of loc * Bignat.bigint
+ | CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
@@ -480,11 +513,9 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
- | CCases of loc * (constr_expr option * constr_expr option) *
+ | CCases of loc * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list * constr_expr) list
- | COrderedCase of loc * case_style * constr_expr option * constr_expr
- * constr_expr list
| CLetTuple of loc * name list * (name option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name option * constr_expr option)
@@ -493,14 +524,15 @@ type constr_expr =
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key
| CSort of loc * rawsort
- | CCast of loc * constr_expr * constr_expr
+ | CCast of loc * constr_expr * cast_kind * constr_expr
| CNotation of loc * notation * constr_expr list
- | CNumeral of loc * Bignat.bigint
+ | CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
+
and fixpoint_expr =
- identifier * int * local_binder list * constr_expr * constr_expr
+ identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and local_binder =
| LocalRawDef of name located * constr_expr
@@ -509,6 +541,10 @@ and local_binder =
and cofixpoint_expr =
identifier * local_binder list * constr_expr * constr_expr
+and recursion_order_expr =
+ | CStructRec
+ | CWfRec of constr_expr
+
(***********************)
(* For binders parsing *)
@@ -520,6 +556,9 @@ let rec local_binders_length = function
let names_of_local_assums bl =
List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
+let names_of_local_binders bl =
+ List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl)
+
(**********************************************************************)
(* Functions on constr_expr *)
@@ -535,16 +574,15 @@ let constr_loc = function
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
| CCases (loc,_,_,_) -> loc
- | COrderedCase (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
| CHole loc -> loc
| CPatVar (loc,_) -> loc
| CEvar (loc,_) -> loc
| CSort (loc,_) -> loc
- | CCast (loc,_,_) -> loc
+ | CCast (loc,_,_,_) -> loc
| CNotation (loc,_,_) -> loc
- | CNumeral (loc,_) -> loc
+ | CPrim (loc,_) -> loc
| CDelimiters (loc,_,_) -> loc
| CDynamic _ -> dummy_loc
@@ -552,8 +590,9 @@ let cases_pattern_loc = function
| CPatAlias (loc,_,_) -> loc
| CPatCstr (loc,_,_) -> loc
| CPatAtom (loc,_) -> loc
+ | CPatOr (loc,_) -> loc
| CPatNotation (loc,_,_) -> loc
- | CPatNumeral (loc,_) -> loc
+ | CPatPrim (loc,_) -> loc
| CPatDelimiters (loc,_,_) -> loc
let occur_var_constr_ref id = function
@@ -571,12 +610,12 @@ let rec occur_var_constr_expr id = function
| CProdN (_,l,b) -> occur_var_binders id b l
| CLambdaN (_,l,b) -> occur_var_binders id b l
| CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a]
- | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
+ | CCast (loc,a,_,b) ->
+ occur_var_constr_expr id a or occur_var_constr_expr id b
| CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l
| CDelimiters (loc,_,a) -> occur_var_constr_expr id a
- | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false
+ | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ -> false
| CCases (loc,_,_,_)
- | COrderedCase (loc,_,_,_,_)
| CLetTuple (loc,_,_,_,_)
| CIf (loc,_,_,_,_)
| CFix (loc,_,_)
@@ -593,26 +632,45 @@ and occur_var_binders id b = function
let mkIdentC id = CRef (Ident (dummy_loc, id))
let mkRefC r = CRef r
let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
-let mkCastC (a,b) = CCast (dummy_loc,a,b)
+let mkCastC (a,k,b) = CCast (dummy_loc,a,k,b)
let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b)
+let rec abstract_constr_expr c = function
+ | [] -> c
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+ | LocalRawAssum (idl,t)::bl ->
+ List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+ (abstract_constr_expr c bl)
+
+let rec prod_constr_expr c = function
+ | [] -> c
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+ | LocalRawAssum (idl,t)::bl ->
+ List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+ (prod_constr_expr c bl)
+
+let coerce_to_id = function
+ | CRef (Ident (loc,id)) -> (loc,id)
+ | a -> user_err_loc
+ (constr_loc a,"coerce_to_id",
+ str "This expression should be a simple identifier")
+
(* Used in correctness and interface *)
let names_of_cases_indtype =
- let rec vars_of ids t =
- match t with
- (* We deal only with the regular cases *)
- | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> vars_of ids a) [] l
- | CRef (Ident (_,id)) -> id::ids
- | CNotation (_,_,l)
- (* assume the ntn is applicative and does not instantiate the head !! *)
- | CAppExpl (_,_,l) -> List.fold_left vars_of [] l
- | CDelimiters(_,_,c) -> vars_of ids c
- | _ -> ids in
- vars_of []
+ let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
+ let rec vars_of = function
+ (* We deal only with the regular cases *)
+ | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
+ | CNotation (_,_,l)
+ (* assume the ntn is applicative and does not instantiate the head !! *)
+ | CAppExpl (_,_,l) -> List.fold_left add_var [] l
+ | CDelimiters(_,_,c) -> vars_of c
+ | _ -> [] in
+ vars_of
let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
@@ -642,12 +700,12 @@ let map_constr_expr_with_binders f g e = function
| CLambdaN (loc,bl,b) ->
let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
| CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
- | CCast (loc,a,b) -> CCast (loc,f e a,f e b)
+ | CCast (loc,a,k,b) -> CCast (loc,f e a,k,f e b)
| CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
- | CNumeral _ | CDynamic _ | CRef _ as x -> x
- | CCases (loc,(po,rtnpo),a,bl) ->
+ | CPrim _ | CDynamic _ | CRef _ as x -> x
+ | CCases (loc,rtnpo,a,bl) ->
(* TODO: apply g on the binding variables in pat... *)
let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
let e' =
@@ -660,10 +718,8 @@ let map_constr_expr_with_binders f g e = function
indnal (option_fold_right (name_fold g) na e))
a e
in
- CCases (loc,(option_app (f e) po, option_app (f e') rtnpo),
+ CCases (loc,option_app (f e') rtnpo,
List.map (fun (tm,x) -> (f e tm,x)) a,bl)
- | COrderedCase (loc,s,po,a,bl) ->
- COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
let e' = List.fold_right (name_fold g) nal e in
let e'' = option_fold_right (name_fold g) ona e in
@@ -698,8 +754,8 @@ let rec replace_vars_constr_expr l = function
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
- | CWith_Module of identifier located * qualid located
- | CWith_Definition of identifier located * constr_expr
+ | CWith_Module of identifier list located * qualid located
+ | CWith_Definition of identifier list located * constr_expr
type module_type_ast =
| CMTEident of qualid located
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 54547352..2f4f667d 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: topconstr.mli,v 1.23.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: topconstr.mli 8624 2006-03-13 17:38:17Z msozeau $ i*)
(*i*)
open Pp
@@ -15,6 +15,7 @@ open Names
open Libnames
open Rawterm
open Term
+open Mod_subst
(*i*)
(*s This is the subtype of rawconstr allowed in syntactic extensions *)
@@ -32,25 +33,28 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option * aconstr option *
+ | ACases of aconstr option *
(aconstr * (name * (inductive * name list) option)) list *
(identifier list * cases_pattern list * aconstr) list
- | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ASort of rawsort
- | AHole of hole_kind
+ | AHole of Evd.hole_kind
| APatVar of patvar
- | ACast of aconstr * aconstr
+ | ACast of aconstr * cast_kind * aconstr
val rawconstr_of_aconstr_with_binders : loc ->
(identifier -> 'a -> identifier * 'a) ->
('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
-val subst_aconstr : Names.substitution -> aconstr -> aconstr
+val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
+
+val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr
val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+val eq_rawconstr : rawconstr -> rawconstr -> bool
+
(* [match_aconstr metas] match a rawconstr against an aconstr with
metavariables in [metas]; it raises [No_match] if the matching fails *)
exception No_match
@@ -59,7 +63,7 @@ type scope_name = string
type interpretation =
(identifier * (scope_name option * scope_name list)) list * aconstr
-val match_aconstr : (*i scope_name option -> i*) rawconstr -> interpretation ->
+val match_aconstr : rawconstr -> interpretation ->
(rawconstr * (scope_name option * scope_name list)) list
(*s Concrete syntax for terms *)
@@ -70,12 +74,15 @@ type explicitation = ExplByPos of int | ExplByName of identifier
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
+type prim_token = Numeral of Bigint.bigint | String of string
+
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
+ | CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr list
- | CPatNumeral of loc * Bignat.bigint
+ | CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
@@ -89,11 +96,9 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
- | CCases of loc * (constr_expr option * constr_expr option) *
+ | CCases of loc * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list * constr_expr) list
- | COrderedCase of loc * case_style * constr_expr option * constr_expr
- * constr_expr list
| CLetTuple of loc * name list * (name option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name option * constr_expr option)
@@ -102,18 +107,22 @@ type constr_expr =
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key
| CSort of loc * rawsort
- | CCast of loc * constr_expr * constr_expr
+ | CCast of loc * constr_expr * cast_kind * constr_expr
| CNotation of loc * notation * constr_expr list
- | CNumeral of loc * Bignat.bigint
+ | CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
and fixpoint_expr =
- identifier * int * local_binder list * constr_expr * constr_expr
+ identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and cofixpoint_expr =
identifier * local_binder list * constr_expr * constr_expr
+and recursion_order_expr =
+ | CStructRec
+ | CWfRec of constr_expr
+
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * constr_expr
@@ -134,11 +143,16 @@ val names_of_cases_indtype : constr_expr -> identifier list
val mkIdentC : identifier -> constr_expr
val mkRefC : reference -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * constr_expr -> constr_expr
+val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr
val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
+val coerce_to_id : constr_expr -> identifier located
+
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+
(* For binders parsing *)
(* Includes let binders *)
@@ -147,6 +161,9 @@ val local_binders_length : local_binder list -> int
(* Does not take let binders into account *)
val names_of_local_assums : local_binder list -> name located list
+(* With let binders *)
+val names_of_local_binders : local_binder list -> name located list
+
(* Used in correctness and interface; absence of var capture not guaranteed *)
(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
@@ -157,8 +174,8 @@ val map_constr_expr_with_binders :
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
- | CWith_Module of identifier located * qualid located
- | CWith_Definition of identifier located * constr_expr
+ | CWith_Module of identifier list located * qualid located
+ | CWith_Definition of identifier list located * constr_expr
type module_type_ast =
| CMTEident of qualid located
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 21:12:42 +0000