From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- interp/constrextern.ml | 1855 +++++++++++++++++++++++++++++++++++++++++++++++ interp/constrextern.mli | 77 ++ interp/constrintern.ml | 1165 +++++++++++++++++++++++++++++ interp/constrintern.mli | 126 ++++ interp/coqlib.ml | 294 ++++++++ interp/coqlib.mli | 126 ++++ interp/doc.tex | 14 + interp/genarg.ml | 228 ++++++ interp/genarg.mli | 262 +++++++ interp/modintern.ml | 103 +++ interp/modintern.mli | 24 + interp/ppextend.ml | 58 ++ interp/ppextend.mli | 48 ++ interp/reserve.ml | 95 +++ interp/reserve.mli | 17 + interp/symbols.ml | 662 +++++++++++++++++ interp/symbols.mli | 160 ++++ interp/syntax_def.ml | 75 ++ interp/syntax_def.mli | 25 + interp/topconstr.ml | 702 ++++++++++++++++++ interp/topconstr.mli | 172 +++++ 21 files changed, 6288 insertions(+) create mode 100644 interp/constrextern.ml create mode 100644 interp/constrextern.mli create mode 100644 interp/constrintern.ml create mode 100644 interp/constrintern.mli create mode 100644 interp/coqlib.ml create mode 100644 interp/coqlib.mli create mode 100644 interp/doc.tex create mode 100644 interp/genarg.ml create mode 100644 interp/genarg.mli create mode 100644 interp/modintern.ml create mode 100644 interp/modintern.mli create mode 100644 interp/ppextend.ml create mode 100644 interp/ppextend.mli create mode 100644 interp/reserve.ml create mode 100644 interp/reserve.mli create mode 100644 interp/symbols.ml create mode 100644 interp/symbols.mli create mode 100644 interp/syntax_def.ml create mode 100644 interp/syntax_def.mli create mode 100644 interp/topconstr.ml create mode 100644 interp/topconstr.mli (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml new file mode 100644 index 00000000..6692dca5 --- /dev/null +++ b/interp/constrextern.ml @@ -0,0 +1,1855 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [] + +(**********************************************************************) +(* Various externalisation functions *) + +let insert_delimiters e = function + | None -> e + | Some sc -> CDelimiters (dummy_loc,sc,e) + +let insert_pat_delimiters e = function + | None -> e + | Some sc -> CPatDelimiters (dummy_loc,sc,e) + +(**********************************************************************) +(* conversion of references *) + +let ids_of_ctxt ctxt = + Array.to_list + (Array.map + (function c -> match kind_of_term c with + | Var id -> id + | _ -> + error + "Termast: arbitrary substitution of references not yet implemented") + ctxt) + +let idopt_of_name = function + | Name id -> Some id + | Anonymous -> None + +let extern_evar loc n = +(* + msgerrnl (str + "Warning: existential variable turned into meta-variable during externalization"); + CPatVar (loc,(false,make_ident "META" (Some n))) +*) + CEvar (loc,n) + +let raw_string_of_ref = function + | ConstRef kn -> + "CONST("^(string_of_kn kn)^")" + | IndRef (kn,i) -> + "IND("^(string_of_kn kn)^","^(string_of_int i)^")" + | ConstructRef ((kn,i),j) -> + "CONSTRUCT("^ + (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")" + | VarRef id -> + "SECVAR("^(string_of_id id)^")" + +(* v7->v8 translation *) + +let name_app f = function + | Name id -> Name (f id) + | Anonymous -> Anonymous + +let rec translate_ident_string = function + (* translate keyword *) + | ("at" | "IF" | "forall" | "fun" | "match" | "fix" | "cofix" | "for" | "let" + | "if" | "then" | "else" | "return" | "mod" | "where" + | "exists" | "exists2" | "using" as s) -> + let s' = s^"_" in + msgerrnl + (str ("Warning: '"^ + s^"' is now a keyword; it has been translated to '"^s'^"'")); + s' +(* Le conflit est en fait surtout avec Eval dans Definition et c'est gere dans + Ppconstrnew + | "eval" as s -> + let s' = s^"_" in + msgerrnl + (str ("Warning: '"^ + s^"' is a conflicting ident; it has been translated to '"^s'^"'")); + s' +*) + + (* avoid _ *) + | "_" -> + msgerrnl (str + "Warning: '_' is no longer an ident; it has been translated to 'x_'"); + "x_" + (* avoid @ *) + | s when String.contains s '@' -> + let n = String.index s '@' in + translate_ident_string + (String.sub s 0 n ^ "'at'" ^ String.sub s (n+1) (String.length s -n-1)) + | s -> s + +let translate_ident id = + id_of_string (translate_ident_string (string_of_id id)) + +let is_coq_root d = + let d = repr_dirpath d in d <> [] & string_of_id (list_last d) = "Coq" + +let is_dir dir s = + let d = repr_dirpath dir in + d <> [] & string_of_id (List.hd d) = s + +let is_module m = is_dir (Lib.library_dp()) m + +let bp = ["BinPos"] +let bz = ["BinInt"] +let bn = ["BinNat"] +let pn = ["nat"] +let zc = ["Zcompare"] +let lo = ["Logic"] +let da = ["Datatypes"] +let zabs = ["Zabs"] +let zo = ["Zorder"] +let zn = ["Znat"] +let wz = ["Wf_Z"] +let mu = ["Mult"] +let pl = ["Plus"] +let mi = ["Minus"] +let le = ["Le"] +let gt = ["Gt"] +let lt = ["Lt"] +let be = ["Between"] +let bo = ["Bool"] +let c dir = + let d = repr_dirpath dir in + if d = [] then [] else [string_of_id (List.hd d)] + +let translation_table = [ + (* ZArith *) +"double_moins_un", (bp,"Pdouble_minus_one"); +"double_moins_deux", (bp,"Pdouble_minus_two"); +"is_double_moins_un", (bp,"Psucc_o_double_minus_one_eq_xO"); +"double_moins_un_add_un_xI", (bp,"Pdouble_minus_one_o_succ_eq_xI"); +"add_un_Zs", (bz,"Zpos_succ_morphism"); +"entier", (bn,"N"); +"entier_of_Z", (bz,"Zabs_N"); +"Z_of_entier", (bz,"Z_of_N"); +"SUPERIEUR", (da,"Gt"); +"EGAL", (da,"Eq"); +"INFERIEUR", (da,"Lt"); +"add", (bp,"Pplus"); +"add_carry", (bp,"Pplus_carry"); +"add_assoc", (bp,"Pplus_assoc"); +"add_sym", (bp,"Pplus_comm"); +"add_x_x", (bp,"Pplus_diag"); +"add_carry_add", (bp,"Pplus_carry_plus"); +"simpl_add_r", (bp,"Pplus_reg_r"); +"simpl_add_l", (bp,"Pplus_reg_l"); +"simpl_add_carry_r", (bp,"Pplus_carry_reg_r"); +"simpl_add_carry_l", (bp,"Pplus_carry_reg_l"); +"simpl_times_r", (bp,"Pmult_reg_r"); +"simpl_times_l", (bp,"Pmult_reg_l"); +(* +"xO_xI_add_double_moins_un", (bp,"xO_xI_plus_double_minus_one"); +*) +"double_moins_un_plus_xO_double_moins_un", + (bp,"Pdouble_minus_one_plus_xO_double_minus_one"); +"add_xI_double_moins_un", (bp,"Pplus_xI_double_minus_one"); +"add_xO_double_moins_un", (bp,"Pplus_xO_double_minus_one"); +"iter_pos_add", (bp,"iter_pos_plus"); +"add_no_neutral", (bp,"Pplus_no_neutral"); +"add_carry_not_add_un", (bp,"Pplus_carry_no_neutral"); +"times_add_distr", (bp,"Pmult_plus_distr_l"); +"times_add_distr_l", (bp,"Pmult_plus_distr_r"); +"times_true_sub_distr", (bp,"Pmult_minus_distr_l"); +"times_sym", (bp,"Pmult_comm"); +"times_assoc", (bp,"Pmult_assoc"); +"times_convert", (bp,"nat_of_P_mult_morphism"); +"true_sub", (bp,"Pminus"); +"times_x_1", (bp,"Pmult_1_r"); +"times_x_double", (bp,"Pmult_xO_permute_r"); + (* Changer en Pmult_xO_distrib_r_reverse *) +"times_x_double_plus_one", (bp,"Pmult_xI_permute_r"); (* Changer ? *) +"times_discr_xO_xI", (bp,"Pmult_xI_mult_xO_discr"); +"times_discr_xO", (bp,"Pmult_xO_discr"); +"times_one_inversion_l", (bp,"Pmult_1_inversion_l"); +"true_sub_convert", (bp,"nat_of_P_minus_morphism"); +"compare_true_sub_right", (bp,"Pcompare_minus_r"); +"compare_true_sub_left", (bp,"Pcompare_minus_l"); +"sub_add", (bp,"Pplus_minus" (* similar to le_plus_minus in Arith *)); +"sub_add_one", (bp,"Ppred_succ"); +"add_sub_one", (bp,"Psucc_pred"); +"add_un", (bp,"Psucc"); +"add_un_discr", (bp,"Psucc_discr"); +"add_un_not_un", (bp,"Psucc_not_one"); +"add_un_inj", (bp,"Psucc_inj"); +"xI_add_un_xO", (bp,"xI_succ_xO"); +"ZL12", (bp,"Pplus_one_succ_r"); +"ZL12bis", (bp,"Pplus_one_succ_l"); +"ZL13", (bp,"Pplus_carry_spec"); + (* Changer en Pplus_succ_distrib_r_reverse ? *) +"ZL14", (bp,"Pplus_succ_permute_r"); + (* Changer en Plus_succ_distrib_l_reverse *) +"ZL14bis", (bp,"Pplus_succ_permute_l"); +"sub_un", (bp,"Ppred"); +"sub_pos", (bp,"Pminus_mask"); +"sub_pos_x_x", (bp,"Pminus_mask_diag"); +(*"sub_pos_x_x", (bp,"Pminus_mask_diag");*) +"sub_pos_SUPERIEUR", (bp,"Pminus_mask_Gt"); +"sub_neg", (bp,"Pminus_mask_carry"); +"Zdiv2_pos", (bp,"Pdiv2"); +"Pdiv2", (["Zbinary"],"Zdiv2_ge_compat"); +"ZERO", (bz,"Z0"); +"POS", (bz,"Zpos"); +"NEG", (bz,"Zneg"); +"Nul", (bn,"N0"); +"Pos", (bn,"Npos"); +"Un_suivi_de", (bn,"Ndouble_plus_one"); +"Zero_suivi_de", (bn,"Ndouble"); +"Un_suivi_de_mask", (bp,"Pdouble_plus_one_mask"); +"Zero_suivi_de_mask", (bp,"Pdouble_mask"); +"ZS", (bp,"double_eq_zero_inversion"); +"US", (bp,"double_plus_one_zero_discr"); +"USH", (bp,"double_plus_one_eq_one_inversion"); +"ZSH", (bp,"double_eq_one_discr"); +"ZPminus_add_un_permute", (bz,"ZPminus_succ_permute"); +"ZPminus_add_un_permute_Zopp", (bz,"ZPminus_succ_permute_opp"); +"ZPminus_double_moins_un_xO_add_un", (bz,"ZPminus_double_minus_one_xO_succ"); +"ZL1", (bp,"xO_succ_permute"); (* ?? *) +"Zplus_assoc_r", (bz,"Zplus_assoc_reverse"); +"Zplus_sym", (bz,"Zplus_comm"); +"Zero_left", (bz,"Zplus_0_l"); +"Zero_right", (bz,"Zplus_0_r"); +"Zplus_n_O", (bz,"Zplus_0_r_reverse"); +"Zplus_unit_left", (bz,"Zplus_0_simpl_l"); +"Zplus_unit_right", (bz,"Zplus_0_simpl_l_reverse"); +"Zplus_Zopp_expand", (bz,"Zplus_opp_expand"); +"Zn_Sn", (bz,"Zsucc_discr"); +"Zs", (bz,"Zsucc"); +"Psucc_Zs", (bz,"Zpos_succ_permute"); +"Zs_pred", (bz,"Zsucc_pred"); +"Zpred_Sn", (bz,"Zpred_succ"); +"Zminus_n_O", (bz,"Zminus_0_l_reverse"); +"Zminus_n_n", (bz,"Zminus_diag_reverse"); +"Zminus_Sn_m", (bz,"Zminus_succ_l"); +"Zeq_Zminus", (bz,"Zeq_minus"); +"Zminus_Zeq", (bz,"Zminus_eq"); +"Zplus_minus", (bz,"Zplus_minus_eq"); +"Zminus_plus", (bz,"Zminus_plus"); +"Zminus_plus_simpl", (bz,"Zminus_plus_simpl_l_reverse"); +"Zminus_Zplus_compatible", (bz,"Zminus_plus_simpl_r"); +"Zle_plus_minus", (bz,"Zplus_minus"); +"Zopp_Zplus", (bz,"Zopp_plus_distr"); +"Zopp_Zopp", (bz,"Zopp_involutive"); +"Zopp_NEG", (bz,"Zopp_neg"); +"Zopp_Zdouble", (bz,"Zopp_double"); +"Zopp_Zdouble_plus_one", (bz,"Zopp_double_plus_one"); +"Zopp_Zdouble_minus_one", (bz,"Zopp_double_minus_one"); +"Zplus_inverse_r", (bz,"Zplus_opp_r"); +"Zplus_inverse_l", (bz,"Zplus_opp_l"); +"Zplus_S_n", (bz,"Zplus_succ_l"); +"Zplus_n_Sm", (bz,"Zplus_succ_r"); +"Zplus_Snm_nSm", (bz,"Zplus_succ_comm"); +"Zmult_assoc_r", (bz,"Zmult_assoc_reverse"); +"Zmult_sym", (bz,"Zmult_comm"); +"Zmult_eq", (bz,"Zmult_integral_l"); +"Zmult_zero", (bz,"Zmult_integral"); +"Zero_mult_left", (bz,"Zmult_0_l"); +"Zero_mult_right", (bz,"Zmult_0_r"); +"Zmult_1_n", (bz,"Zmult_1_l"); +"Zmult_n_1", (bz,"Zmult_1_r"); +"Zmult_n_O", (bz,"Zmult_0_r_reverse"); +"Zopp_one", (bz,"Zopp_eq_mult_neg_1"); +"Zopp_Zmult", (bz,"Zopp_mult_distr_l_reverse"); +"Zopp_Zmult_r", (bz,"Zopp_mult_distr_r"); +"Zopp_Zmult_l", (bz,"Zopp_mult_distr_l"); +"Zmult_Zopp_Zopp", (bz,"Zmult_opp_opp"); +"Zmult_Zopp_left", (bz,"Zmult_opp_comm"); +"Zmult_Zplus_distr", (bz,"Zmult_plus_distr_r"); +"Zmult_plus_distr", (bz,"Zmult_plus_distr_r"); +"Zmult_Zminus_distr_r", (bz,"Zmult_minus_distr_l"); +"Zmult_Zminus_distr_l", (bz,"Zmult_minus_distr_r"); +"Zcompare_Zplus_compatible", (zc,"Zcompare_plus_compat"); +"Zcompare_Zplus_compatible2", (zc,"Zplus_compare_compat"); +"Zcompare_Zmult_compatible", (zc,"Zcompare_mult_compat"); +"inject_nat", (bz,"Z_of_nat"); +"inject_nat_complete", (wz,"Z_of_nat_complete"); +"inject_nat_complete_inf", (wz,"Z_of_nat_complete_inf"); +"inject_nat_prop", (wz,"Z_of_nat_prop"); +"inject_nat_set", (wz,"Z_of_nat_set"); +"convert", (bp,"nat_of_P"); +"anti_convert", (bp,"P_of_succ_nat"); +"positive_to_nat", (bp,"Pmult_nat"); +"Zopp_intro", (bz,"Zopp_inj"); +"plus_iter_add", (bp,"plus_iter_eq_plus"); +"compare", (bp,"Pcompare"); +"iter_convert", (["Zmisc"],"iter_nat_of_P"); +"ZLSI", (bp,"Pcompare_Gt_Lt"); +"ZLIS", (bp,"Pcompare_Lt_Gt"); +"ZLII", (bp,"Pcompare_Lt_Lt"); +"ZLSS", (bp,"Pcompare_Gt_Gt"); + (* Pnat *) +"convert_intro", (pn,"nat_of_P_inj"); +"convert_add", (pn,"nat_of_P_plus_morphism"); +"convert_add_un", (pn,"Pmult_nat_succ_morphism"); +"cvt_add_un", (pn,"nat_of_P_succ_morphism"); +"convert_add_carry", (pn,"Pmult_nat_plus_carry_morphism"); +"compare_convert_O", (pn,"lt_O_nat_of_P"); +"add_verif", (pn,"Pmult_nat_l_plus_morphism"); +"ZL2", (pn,"Pmult_nat_r_plus_morphism"); +"compare_positive_to_nat_O", (pn,"le_Pmult_nat"); +(* Trop spécifique ? +"ZL6", (pn,"Pmult_nat_plus_shift_morphism"); +*) +"ZL15", (pn,"Pplus_carry_pred_eq_plus"); +"cvt_carry", (pn,"nat_of_P_plus_carry_morphism"); +"compare_convert1", (pn,"Pcompare_not_Eq"); +"compare_convert_INFERIEUR", (pn,"nat_of_P_lt_Lt_compare_morphism"); +"compare_convert_SUPERIEUR", (pn,"nat_of_P_gt_Gt_compare_morphism"); +"compare_convert_EGAL", (pn,"Pcompare_Eq_eq"); +"convert_compare_INFERIEUR", (pn,"nat_of_P_lt_Lt_compare_complement_morphism"); +"convert_compare_SUPERIEUR", (pn,"nat_of_P_gt_Gt_compare_complement_morphism"); +"convert_compare_EGAL", (pn,"Pcompare_refl"); +"bij1", (pn,"nat_of_P_o_P_of_succ_nat_eq_succ"); +"bij2", (pn,"P_of_succ_nat_o_nat_of_P_eq_succ"); +"bij3", (pn,"pred_o_P_of_succ_nat_o_nat_of_P_eq_id"); + (* Zcompare *) +"Zcompare_EGAL", (zc,"Zcompare_Eq_iff_eq"); +"Zcompare_EGAL_eq", (zc,"Zcompare_Eq_eq"); +"Zcompare_x_x", (zc,"Zcompare_refl"); +"Zcompare_et_un", (zc,"Zcompare_Gt_not_Lt"); +"Zcompare_trans_SUPERIEUR", (zc,"Zcompare_Gt_trans"); +"Zcompare_n_S", (zc,"Zcompare_succ_compat"); +"SUPERIEUR_POS", (zc,"Zcompare_Gt_spec"); +"Zcompare_ANTISYM", (zc,"Zcompare_Gt_Lt_antisym"); +"Zcompare_Zs_SUPERIEUR", (zc,"Zcompare_succ_Gt"); +"Zcompare_Zopp", (zc,"Zcompare_opp"); +"POS_inject", (zn,"Zpos_eq_Z_of_nat_o_nat_of_P"); +"absolu", (bz,"Zabs_nat"); +"absolu_lt", (zabs,"Zabs_nat_lt" (* "Zabs_nat_lt_morphism_pos" ? *)); +"Zeq_add_S", (bz,"Zsucc_inj"); +"Znot_eq_S", (bz,"Zsucc_inj_contrapositive"); +"Zeq_S", (bz,"Zsucc_eq_compat"); +"Zsimpl_plus_l", (bz,"Zplus_reg_l"); +"Zplus_simpl", (bz,"Zplus_eq_compat"); +"POS_gt_ZERO", (zo,"Zgt_pos_0"); +"ZERO_le_POS", (zo,"Zle_0_pos"); +"ZERO_le_inj", (zo,"Zle_0_nat"); +"NEG_lt_ZERO", (zo,"Zlt_neg_0"); +"Zlt_ZERO_pred_le_ZERO", (zo,"Zlt_0_le_0_pred"); +"POS_xI", (bz,"Zpos_xI"); +"POS_xO", (bz,"Zpos_xO"); +"NEG_xI", (bz,"Zneg_xI"); +"NEG_xO", (bz,"Zneg_xO"); +"POS_add", (bz,"Zpos_plus_distr"); +"NEG_add", (bz,"Zneg_plus_distr"); + (* Z Orders *) +"not_Zge", (zo,"Znot_ge_lt"); +"not_Zlt", (zo,"Znot_lt_ge"); +"not_Zle", (zo,"Znot_le_gt"); +"not_Zgt", (zo,"Znot_gt_le"); +"Zgt_not_sym", (zo,"Zgt_asym"); +"Zlt_not_sym", (zo,"Zlt_asym"); +"Zlt_n_n", (zo,"Zlt_irrefl"); +"Zgt_antirefl", (zo,"Zgt_irrefl"); +"Zgt_reg_l", (zo,"Zplus_gt_compat_l"); +"Zgt_reg_r", (zo,"Zplus_gt_compat_r"); +"Zlt_reg_l", (zo,"Zplus_lt_compat_l"); +"Zlt_reg_r", (zo,"Zplus_lt_compat_r"); +"Zle_reg_l", (zo,"Zplus_le_compat_l"); +"Zle_reg_r", (zo,"Zplus_le_compat_r"); +"Zlt_le_reg", (zo,"Zplus_lt_le_compat"); +"Zle_lt_reg", (zo,"Zplus_le_lt_compat"); +"Zle_plus_plus", (zo,"Zplus_le_compat"); +"Zlt_Zplus", (zo,"Zplus_lt_compat"); +"Zle_O_plus", (zo,"Zplus_le_0_compat"); +"Zle_mult_simpl", (zo,"Zmult_le_reg_r"); +"Zge_mult_simpl", (zo,"Zmult_ge_reg_r"); +"Zgt_mult_simpl", (zo,"Zmult_gt_reg_r"); +"Zsimpl_gt_plus_l", (zo,"Zplus_gt_reg_l"); +"Zsimpl_gt_plus_r", (zo,"Zplus_gt_reg_r"); +"Zsimpl_le_plus_l", (zo,"Zplus_le_reg_l"); +"Zsimpl_le_plus_r", (zo,"Zplus_le_reg_r"); +"Zsimpl_lt_plus_l", (zo,"Zplus_lt_reg_l"); +"Zsimpl_lt_plus_r", (zo,"Zplus_lt_reg_r"); +"Zlt_Zmult_right2", (zo,"Zmult_gt_0_lt_reg_r"); +"Zlt_Zmult_right", (zo,"Zmult_gt_0_lt_compat_r"); +"Zle_Zmult_right2", (zo,"Zmult_gt_0_le_reg_r"); +"Zle_Zmult_right", (zo,"Zmult_gt_0_le_compat_r"); +"Zgt_Zmult_right", (zo,"Zmult_gt_compat_r"); +"Zgt_Zmult_left", (zo,"Zmult_gt_compat_l"); +"Zlt_Zmult_left", (zo,"Zmult_gt_0_lt_compat_l"); +"Zcompare_Zmult_right", (zc,"Zmult_compare_compat_r"); +"Zcompare_Zmult_left", (zc,"Zmult_compare_compat_l"); +"Zplus_Zmult_2", (bz,"Zplus_diag_eq_mult_2"); +"Zmult_Sm_n", (bz,"Zmult_succ_l_reverse"); +"Zmult_n_Sm", (bz,"Zmult_succ_r_reverse"); +"Zmult_le", (zo,"Zmult_le_0_reg_r"); +"Zmult_reg_left", (bz,"Zmult_reg_l"); +"Zmult_reg_right", (bz,"Zmult_reg_r"); +"Zle_ZERO_mult", (zo,"Zmult_le_0_compat"); +"Zgt_ZERO_mult", (zo,"Zmult_gt_0_compat"); +"Zle_mult", (zo,"Zmult_gt_0_le_0_compat"); +"Zmult_lt", (zo,"Zmult_gt_0_lt_0_reg_r"); +"Zmult_gt", (zo,"Zmult_gt_0_reg_l"); +"Zle_Zmult_pos_right", (zo,"Zmult_le_compat_r"); +"Zle_Zmult_pos_left", (zo,"Zmult_le_compat_l"); +"Zge_Zmult_pos_right", (zo,"Zmult_ge_compat_r"); +"Zge_Zmult_pos_left", (zo,"Zmult_ge_compat_l"); +"Zge_Zmult_pos_compat", (zo,"Zmult_ge_compat"); +"Zlt_Zcompare", (zo,"Zlt_compare"); +"Zle_Zcompare", (zo,"Zle_compare"); +"Zgt_Zcompare", (zo,"Zgt_compare"); +"Zge_Zcompare", (zo,"Zge_compare"); + (* ex-IntMap *) +"convert_xH", (pn,"nat_of_P_xH"); +"convert_xO", (pn,"nat_of_P_xO"); +"convert_xI", (pn,"nat_of_P_xI"); +"positive_to_nat_mult", (pn,"Pmult_nat_mult_permute"); +"positive_to_nat_2", (pn,"Pmult_nat_2_mult_2_permute"); +"positive_to_nat_4", (pn,"Pmult_nat_4_mult_2_permute"); + (* ZArith and Arith orders *) +"Zle_refl", (zo,"Zeq_le"); +"Zle_n", (zo,"Zle_refl"); +"Zle_trans_S", (zo,"Zle_succ_le"); +"Zgt_trans_S", (zo,"Zge_trans_succ"); +"Zgt_S", (zo,"Zgt_succ_gt_or_eq"); +"Zle_Sn_n", (zo,"Znot_le_succ"); +"Zlt_n_Sn", (zo,"Zlt_succ"); +"Zlt_S", (zo,"Zlt_lt_succ"); +"Zlt_n_S", (zo,"Zsucc_lt_compat"); +"Zle_n_S", (zo,"Zsucc_le_compat"); +"Zgt_n_S", (zo,"Zsucc_gt_compat"); +"Zlt_S_n", (zo,"Zsucc_lt_reg"); +"Zgt_S_n", (zo,"Zsucc_gt_reg"); +"Zle_S_n", (zo,"Zsucc_le_reg"); +"Zle_0_plus", (zo,"Zplus_le_0_compat"); +"Zgt_Sn_n", (zo,"Zgt_succ"); +"Zgt_le_S", (zo,"Zgt_le_succ"); +"Zgt_S_le", (zo,"Zgt_succ_le"); +"Zle_S_gt", (zo,"Zlt_succ_gt"); +"Zle_gt_S", (zo,"Zlt_gt_succ"); +"Zgt_pred", (zo,"Zgt_succ_pred"); +"Zlt_pred", (zo,"Zlt_succ_pred"); +"Zgt0_le_pred", (zo,"Zgt_0_le_0_pred"); +"Z_O_1", (zo,"Zlt_0_1"); +"Zle_NEG_POS", (zo,"Zle_neg_pos"); +"Zle_n_Sn", (zo,"Zle_succ"); +"Zle_pred_n", (zo,"Zle_pred"); +"Zlt_pred_n_n", (zo,"Zlt_pred"); +"Zlt_le_S", (zo,"Zlt_le_succ"); +"Zlt_n_Sm_le", (zo,"Zlt_succ_le"); +"Zle_lt_n_Sm", (zo,"Zle_lt_succ"); +"Zle_le_S", (zo,"Zle_le_succ"); +"Zlt_minus", (zo,"Zlt_minus_simpl_swap"); +"le_trans_S", (le,"le_Sn_le"); +(* Znumtheory *) +"Zdivide_Zmod", ([],"Zdivide_mod"); +"Zmod_Zdivide", ([],"Zmod_divide"); +"Zdivide_mult_left", ([],"Zmult_divide_compat_l"); +"Zdivide_mult_right", ([],"Zmult_divide_compat_r"); +"Zdivide_opp", ([],"Zdivide_opp_r"); +"Zdivide_opp_rev", ([],"Zdivide_opp_r_rev"); +"Zdivide_opp_left", ([],"Zdivide_opp_l"); +"Zdivide_opp_left_rev", ([],"Zdivide_opp_l_rev"); +"Zdivide_right", ([],"Zdivide_mult_r"); +"Zdivide_left", ([],"Zdivide_mult_l"); +"Zdivide_plus", ([],"Zdivide_plus_r"); +"Zdivide_minus", ([],"Zdivide_minus_l"); +"Zdivide_a_ab", ([],"Zdivide_factor_r"); +"Zdivide_a_ba", ([],"Zdivide_factor_l"); +(* Arith *) +(* Peano.v +"plus_n_O", ("plus_0_r_reverse"); +"plus_O_n", ("plus_0_l"); +*) +"plus_assoc_l", (pl,"plus_assoc"); +"plus_assoc_r", (pl,"plus_assoc_reverse"); +"plus_sym", (pl,"plus_comm"); +"mult_sym", (mu,"mult_comm"); +"max_sym", (["Max"],"max_comm"); +"min_sym", (["Min"],"min_comm"); +"gt_not_sym", (gt,"gt_asym"); +"lt_not_sym", (lt,"lt_asym"); +"gt_antirefl", (gt,"gt_irrefl"); +"lt_n_n", (lt,"lt_irrefl"); +(* Trop utilisé dans CoqBook | "le_n" -> "le_refl"*) +"simpl_plus_l", (pl,"plus_reg_l"); +"simpl_plus_r", (pl,"plus_reg_r"); +"fact_growing", (["Factorial"],"fact_le"); +"mult_assoc_l", (mu,"mult_assoc"); +"mult_assoc_r", (mu,"mult_assoc_reverse"); +"mult_plus_distr", (mu,"mult_plus_distr_r"); +"mult_plus_distr_r", (mu,"mult_plus_distr_l"); +"mult_minus_distr", (mu,"mult_minus_distr_r"); +"mult_1_n", (mu,"mult_1_l"); +"mult_n_1", (mu,"mult_1_r"); +(* Peano.v +"mult_n_O", ("mult_O_r_reverse"); +"mult_n_Sm", ("mult_S_r_reverse"); +*) +"mult_le", (mu,"mult_le_compat_l"); +"le_mult_right", (mu,"mult_le_compat_r"); +"le_mult_mult", (mu,"mult_le_compat"); +"mult_lt", (mu,"mult_S_lt_compat_l"); +"lt_mult_right", (mu,"mult_lt_compat_r"); +"mult_le_conv_1", (mu,"mult_S_le_reg_l"); +"exists", (be,"exists_between"); +"IHexists", ([],"IHexists_between"); +(* Peano.v +"pred_Sn", ("pred_S"); +*) +"inj_minus_aux", (mi,"not_le_minus_0"); +"minus_x_x", (mi,"minus_diag"); +"minus_plus_simpl", (mi,"minus_plus_simpl_l_reverse"); +"gt_reg_l", (gt,"plus_gt_compat_l"); +"le_reg_l", (pl,"plus_le_compat_l"); +"le_reg_r", (pl,"plus_le_compat_r"); +"lt_reg_l", (pl,"plus_lt_compat_l"); +"lt_reg_r", (pl,"plus_lt_compat_r"); +"le_plus_plus", (pl,"plus_le_compat"); +"le_lt_plus_plus", (pl,"plus_le_lt_compat"); +"lt_le_plus_plus", (pl,"plus_lt_le_compat"); +"lt_plus_plus", (pl,"plus_lt_compat"); +"plus_simpl_l", (pl,"plus_reg_l"); +"simpl_gt_plus_l", (pl,"plus_gt_reg_l"); +"simpl_le_plus_l", (pl,"plus_le_reg_l"); +"simpl_lt_plus_l", (pl,"plus_lt_reg_l"); +(* Noms sur le principe de ceux de Z +"le_n_S", ("S_le_compat"); +"le_n_Sn", ("le_S"); +(*"le_O_n", ("??" *)); +"le_pred_n", ("le_pred"); +"le_trans_S", ("le_S_le"); +"le_S_n", ("S_le_reg"); +"le_Sn_O", ("not_le_S_O"); +"le_Sn_n", ("not_le_S"); +*) + (* Init *) +"IF", (lo,"IF_then_else"); + (* Lists *) +"idempot_rev", (["List"],"rev_involutive"); +"forall", (["Streams"],"HereAndFurther"); + (* Bool *) +"orb_sym", (bo,"orb_comm"); +"andb_sym", (bo,"andb_comm"); + (* Ring *) +"SR_plus_sym", (["Ring_theory"],"SR_plus_comm"); +"SR_mult_sym", (["Ring_theory"],"SR_mult_comm"); +"Th_plus_sym", (["Ring_theory"],"Th_plus_comm"); +"Th_mul_sym", (["Ring_theory"],"Th_mult_comm"); +"SSR_plus_sym", (["Setoid_ring_theory"],"SSR_plus_comm"); +"SSR_mult_sym", (["Setoid_ring_theory"],"SSR_mult_comm"); +"STh_plus_sym", (["Setoid_ring_theory"],"STh_plus_comm"); +"STh_mul_sym", (["Setoid_ring_theory"],"STh_mult_comm"); + (* Reals *) +(* +"Rabsolu", ("Rabs"); +"Rabsolu_pos_lt", ("Rabs_pos_lt"); +"Rabsolu_no_R0", ("Rabs_no_R0"); +"Rabsolu_Rabsolu", ("Rabs_Rabs"); +"Rabsolu_mult", ("Rabs_mult"); +"Rabsolu_triang", ("Rabs_triang"); +"Rabsolu_Ropp", ("Rabs_Ropp"); +"Rabsolu_right", ("Rabs_right"); +... +"case_Rabsolu", ("case_Rabs"); +"Pow_Rabsolu", ("Pow_Rabs"); +... +*) +(* Raxioms *) +"complet", ([],"completeness"); +"complet_weak", ([],"completeness_weak"); +"Rle_sym1", ([],"Rle_ge"); +"Rmin_sym", ([],"Rmin_comm"); +"Rplus_sym", ([],"Rplus_comm"); +"Rmult_sym", ([],"Rmult_comm"); +"Rsqr_times", ([],"Rsqr_mult"); +"sqrt_times", ([],"sqrt_mult"); +"Rmult_1l", ([],"Rmult_1_l"); +"Rplus_Ol", ([],"Rplus_0_l"); +"Rplus_Ropp_r", ([],"Rplus_opp_r"); +"Rmult_Rplus_distr", ([],"Rmult_plus_distr_l"); +"Rlt_antisym", ([],"Rlt_asym"); +(* RIneq *) +"Rlt_antirefl", ([],"Rlt_irrefl"); +"Rlt_compatibility", ([],"Rplus_lt_compat_l"); +"Rgt_plus_plus_r", ([],"Rplus_gt_compat_l"); +"Rgt_r_plus_plus", ([],"Rplus_gt_reg_l"); +"Rge_plus_plus_r", ([],"Rplus_ge_compat_l"); +"Rge_r_plus_plus", ([],"Rplus_ge_reg_l"); +(* Si on en change un, il faut changer tous les autres R*_monotony *) +"Rlt_monotony", ([],"Rmult_lt_compat_l"); +"Rlt_monotony_r", ([],"Rmult_lt_compat_r"); +"Rlt_monotony_contra", ([],"Rmult_lt_reg_l"); +(*"Rlt_monotony_rev", ([],"Rmult_lt_reg_l");*) +"Rlt_anti_monotony", ([],"Rmult_lt_gt_compat_neg_l"); +"Rle_monotony", ([],"Rmult_le_compat_l"); +"Rle_monotony_r", ([],"Rmult_le_compat_r"); +"Rle_monotony_contra", ([],"Rmult_le_reg_l"); +"Rle_anti_monotony1", ([],"Rmult_le_compat_neg_l"); +"Rle_anti_monotony", ([],"Rmult_le_ge_compat_neg_l"); +"Rge_monotony", ([],"Rmult_ge_compat_r"); +"Rge_ge_eq", ([],"Rge_antisym"); +(* Le reste de RIneq *) +"imp_not_Req", ([],"Rlt_dichotomy_converse"); +"Req_EM", ([],"Req_dec"); +"total_order", ([],"Rtotal_order"); +"not_Req", ([],"Rdichotomy"); +(* "Rlt_le" -> c dir,"Rlt_le_weak" ? *) +"not_Rle", ([],"Rnot_le_lt"); +"not_Rge", ([],"Rnot_ge_lt"); +"Rlt_le_not", ([],"Rlt_not_le"); +"Rle_not", ([],"Rgt_not_le"); +"Rle_not_lt", ([],"Rle_not_lt"); +"Rlt_ge_not", ([],"Rlt_not_ge"); +"eq_Rle", ([],"Req_le"); +"eq_Rge", ([],"Req_ge"); +"eq_Rle_sym", ([],"Req_le_sym"); +"eq_Rge_sym", ([],"Req_ge_sym"); +(* "Rle_le_eq" -> ? x<=y/\y<=x <-> x=y *) +"Rlt_rew", ([],"Rlt_eq_compat"); +"total_order_Rlt", ([],"Rlt_dec"); +"total_order_Rle", ([],"Rle_dec"); +"total_order_Rgt", ([],"Rgt_dec"); +"total_order_Rge", ([],"Rge_dec"); +"total_order_Rlt_Rle", ([],"Rlt_le_dec"); +(* "Rle_or_lt" -> c dir,"Rle_or_lt"*) +"total_order_Rle_Rlt_eq", ([],"Rle_lt_or_eq_dec"); +(* "inser_trans_R" -> c dir,"Rle_lt_inser_trans" ?*) +(* "Rplus_ne" -> c dir,"Rplus_0_r_l" ? *) +"Rplus_Or", ([],"Rplus_0_r"); +"Rplus_Ropp_l", ([],"Rplus_opp_l"); +"Rplus_Ropp", ([],"Rplus_opp_r_uniq"); +"Rplus_plus_r", ([],"Rplus_eq_compat_l"); +"r_Rplus_plus", ([],"Rplus_eq_reg_l"); +"Rplus_ne_i", ([],"Rplus_0_r_uniq"); +"Rmult_Or", ([],"Rmult_0_r"); +"Rmult_Ol", ([],"Rmult_0_l"); +(* "Rmult_ne" -> c dir,"Rmult_1_l_r" ? *) +"Rmult_1r", ([],"Rmult_1_r"); +"Rmult_mult_r", ([],"Rmult_eq_compat_l"); +"r_Rmult_mult", ([],"Rmult_eq_reg_l"); +"without_div_Od", ([],"Rmult_integral"); +"without_div_Oi", ([],"Rmult_eq_0_compat"); +"without_div_Oi1", ([],"Rmult_eq_0_compat_r"); +"without_div_Oi2", ([],"Rmult_eq_0_compat_l"); +"without_div_O_contr", ([],"Rmult_neq_0_reg"); +"mult_non_zero", ([],"Rmult_integral_contrapositive"); +"Rmult_Rplus_distrl", ([],"Rmult_plus_distr_r"); +"Rsqr_O", ([],"Rsqr_0"); +"Rsqr_r_R0", ([],"Rsqr_0_uniq"); +"eq_Ropp", ([],"Ropp_eq_compat"); +"Ropp_O", ([],"Ropp_0"); +"eq_RoppO", ([],"Ropp_eq_0_compat"); +"Ropp_Ropp", ([],"Ropp_involutive"); +"Ropp_neq", ([],"Ropp_neq_0_compat"); +"Ropp_distr1", ([],"Ropp_plus_distr"); +"Ropp_mul1", ([],"Ropp_mult_distr_l_reverse"); +"Ropp_mul2", ([],"Rmult_opp_opp"); +"Ropp_mul3", ([],"Ropp_mult_distr_r_reverse"); +"minus_R0", ([],"Rminus_0_r"); +"Rminus_Ropp", ([],"Rminus_0_l"); +"Ropp_distr2", ([],"Ropp_minus_distr"); +"Ropp_distr3", ([],"Ropp_minus_distr'"); +"eq_Rminus", ([],"Rminus_diag_eq"); +"Rminus_eq", ([],"Rminus_diag_uniq"); +"Rminus_eq_right", ([],"Rminus_diag_uniq_sym"); +"Rplus_Rminus", ([],"Rplus_minus"); +(* +"Rminus_eq_contra", ([],"Rminus_diag_neq"); +"Rminus_not_eq", ([],"Rminus_neq_diag_sym"); + "Rminus_not_eq_right" -> ? +*) +"Rminus_distr", ([],"Rmult_minus_distr_l"); +"Rinv_R1", ([],"Rinv_1"); +"Rinv_neq_R0", ([],"Rinv_neq_0_compat"); +"Rinv_Rinv", ([],"Rinv_involutive"); +"Rinv_Rmult", ([],"Rinv_mult_distr"); +"Ropp_Rinv", ([],"Ropp_inv_permute"); +(* "Rinv_r_simpl_r" -> OK ? *) +(* "Rinv_r_simpl_l" -> OK ? *) +(* "Rinv_r_simpl_m" -> OK ? *) +"Rinv_Rmult_simpl", ([],"Rinv_mult_simpl"); (* ? *) +"Rlt_compatibility_r", ([],"Rplus_lt_compat_r"); +"Rlt_anti_compatibility", ([],"Rplus_lt_reg_r"); +"Rle_compatibility", ([],"Rplus_le_compat_l"); +"Rle_compatibility_r", ([],"Rplus_le_compat_r"); +"Rle_anti_compatibility", ([],"Rplus_le_reg_l"); +(* "sum_inequa_Rle_lt" -> ? *) +"Rplus_lt", ([],"Rplus_lt_compat"); +"Rplus_le", ([],"Rplus_le_compat"); +"Rplus_lt_le_lt", ([],"Rplus_lt_le_compat"); +"Rplus_le_lt_lt", ([],"Rplus_le_lt_compat"); +"Rgt_Ropp", ([],"Ropp_gt_lt_contravar"); +"Rlt_Ropp", ([],"Ropp_lt_gt_contravar"); +"Ropp_Rlt", ([],"Ropp_lt_cancel"); (* ?? *) +"Rlt_Ropp1", ([],"Ropp_lt_contravar"); +"Rle_Ropp", ([],"Ropp_le_ge_contravar"); +"Ropp_Rle", ([],"Ropp_le_cancel"); +"Rle_Ropp1", ([],"Ropp_le_contravar"); +"Rge_Ropp", ([],"Ropp_ge_le_contravar"); +"Rlt_RO_Ropp", ([],"Ropp_0_lt_gt_contravar"); +"Rgt_RO_Ropp", ([],"Ropp_0_gt_lt_contravar"); +"Rle_RO_Ropp", ([],"Ropp_0_le_ge_contravar"); +"Rge_RO_Ropp", ([],"Ropp_0_ge_le_contravar"); +(* ... cf plus haut pour les lemmes intermediaires *) +"Rle_Rmult_comp", ([],"Rmult_le_compat"); + (* Expliciter que la contrainte est r2>0 dans r1 + "Rle_minus" -> + "Rminus_lt" -> + "Rminus_le" -> + "tech_Rplus" -> +*) +"pos_Rsqr", ([],"Rle_0_sqr"); +"pos_Rsqr1", ([],"Rlt_0_sqr"); +"Rlt_R0_R1", ([],"Rlt_0_1"); +"Rle_R0_R1", ([],"Rle_0_1"); +"Rlt_Rinv", ([],"Rinv_0_lt_compat"); +"Rlt_Rinv2", ([],"Rinv_lt_0_compat"); +"Rinv_lt", ([],"Rinv_lt_contravar"); +"Rlt_Rinv_R1", ([],"Rinv_1_lt_contravar"); +"Rlt_not_ge", ([],"Rnot_lt_ge"); +"Rgt_not_le", ([],"Rnot_gt_le"); +(* + "Rgt_ge" -> "Rgt_ge_weak" ? +*) +"Rlt_sym", ([],"Rlt_gt_iff"); +(* | "Rle_sym1" -> c dir,"Rle_ge" OK *) +"Rle_sym2", ([],"Rge_le"); +"Rle_sym", ([],"Rle_ge_iff"); +(* + "Rge_gt_trans" -> OK + "Rgt_ge_trans" -> OK + "Rgt_trans" -> OK + "Rge_trans" -> OK +*) +"Rgt_RoppO", ([],"Ropp_lt_gt_0_contravar"); +"Rlt_RoppO", ([],"Ropp_gt_lt_0_contravar"); +"Rlt_r_plus_R1", ([],"Rle_lt_0_plus_1"); +"Rlt_r_r_plus_R1", ([],"Rlt_plus_1"); +(* "tech_Rgt_minus" -> ? *) +(* OK, cf plus haut +"Rgt_r_plus_plus", ([],"Rplus_gt_reg_l"); +"Rgt_plus_plus_r", ([],"Rplus_gt_compat_l"); +"Rge_plus_plus_r", ([],"Rplus_ge_compat_l"); +"Rge_r_plus_plus", ([],"Rplus_ge_reg_l"); +"Rge_monotony" -> *) +(* + "Rgt_minus" -> + "minus_Rgt" -> + "Rge_minus" -> + "minus_Rge" -> +*) +"Rmult_gt", ([],"Rmult_gt_0_compat"); +"Rmult_lt_pos", ([],"Rmult_lt_0_compat"); (* lt_0 ou 0_lt ?? *) +"Rplus_eq_R0_l", ([],"Rplus_eq_0_l"); (* ? *) +"Rplus_eq_R0", ([],"Rplus_eq_R0"); +"Rplus_Rsr_eq_R0_l", ([],"Rplus_sqr_eq_0_l"); +"Rplus_Rsr_eq_R0", ([],"Rplus_sqr_eq_0"); +(* + "S_INR" -> + "S_O_plus_INR" -> + "plus_INR" -> + "minus_INR" -> + "mult_INR" -> + "lt_INR_0" -> + "lt_INR" -> + "INR_lt_1" -> + "INR_pos" -> + "pos_INR" -> + "INR_lt" -> + "le_INR" -> + "not_INR_O" -> + "not_O_INR" -> + "not_nm_INR" -> + "INR_eq" -> + "INR_le" -> + "not_1_INR" -> + "IZN" -> + "INR_IZR_INZ" -> + "plus_IZR_NEG_POS" -> + "plus_IZR" -> + "mult_IZR" -> + "Ropp_Ropp_IZR" -> + "Z_R_minus" -> + "lt_O_IZR" -> + "lt_IZR" -> + "eq_IZR_R0" -> + "eq_IZR" -> + "not_O_IZR" -> + "le_O_IZR" -> + "le_IZR" -> + "le_IZR_R1" -> + "IZR_ge" -> + "IZR_le" -> + "IZR_lt" -> + "one_IZR_lt1" -> + "one_IZR_r_R1" -> + "single_z_r_R1" -> + "tech_single_z_r_R1" -> + "prod_neq_R0" -> + "Rmult_le_pos" -> + "double" -> + "double_var" -> +*) +"gt0_plus_gt0_is_gt0", ([],"Rplus_lt_0_compat"); +"ge0_plus_gt0_is_gt0", ([],"Rplus_le_lt_0_compat"); +"gt0_plus_ge0_is_gt0", ([],"Rplus_lt_le_0_compat"); +"ge0_plus_ge0_is_ge0", ([],"Rplus_le_le_0_compat"); +(* + "plus_le_is_le" -> ? + "plus_lt_is_lt" -> ? +*) +"Rmult_lt2", ([],"Rmult_le_0_lt_compat"); +(* "Rge_ge_eq" -> c dir,"Rge_antisym" OK *) +] + +let translate_v7_string dir s = + try + let d,s' = List.assoc s translation_table in + (if d=[] then c dir else d),s' + with Not_found -> + (* Special cases *) + match s with + (* Init *) + | "relation" when is_module "Datatypes" or is_dir dir "Datatypes" + -> da,"comparison" + | "Op" when is_module "Datatypes" or is_dir dir "Datatypes" + -> da,"CompOpp" + (* BinPos *) + | "times" when not (is_module "Mapfold") -> bp,"Pmult" + (* Reals *) + | s when String.length s >= 7 & (String.sub s 0 7 = "Rabsolu") -> + c dir, + "Rabs"^(String.sub s 7 (String.length s - 7)) + | s when String.length s >= 7 & + (String.sub s (String.length s - 7) 7 = "Rabsolu") -> c dir, + "R"^(String.sub s 0 (String.length s - 7))^"abs" + | s when String.length s >= 7 & + let s' = String.sub s 0 7 in + (s' = "unicite" or s' = "unicity") -> c dir, + "uniqueness"^(String.sub s 7 (String.length s - 7)) + | s when String.length s >= 3 & + let s' = String.sub s 0 3 in + s' = "gcd" -> c dir, "Zis_gcd"^(String.sub s 3 (String.length s - 3)) + (* Default *) + | x -> [],x + + +let id_of_v7_string s = + id_of_string (if !Options.v7 then s else snd (translate_v7_string empty_dirpath s)) + +let v7_to_v8_dir_id dir id = + if Options.do_translate() then + let s = string_of_id id in + let dir',s = + if (is_coq_root (Lib.library_dp()) or is_coq_root dir) + then translate_v7_string dir s else [], s in + dir',id_of_string (translate_ident_string s) + else [],id + +let v7_to_v8_id id = snd (v7_to_v8_dir_id empty_dirpath id) + +let short_names = + List.map (fun x -> snd (snd x)) translation_table + +let is_new_name s = + Options.do_translate () & + (List.mem s short_names or + s = "comparison" or s = "CompOpp" or s = "Pmult" or + (String.length s >= 4 & String.sub s 0 4 = "Rabs") or + (String.length s >= 4 & String.sub s (String.length s - 3) 3 = "abs" + & s.[0] = 'R') or + (String.length s >= 10 & String.sub s 0 10 = "uniqueness")) + +let v7_to_v8_dir fulldir dir = + if Options.do_translate () & dir <> empty_dirpath then + let update s = + let l = List.map string_of_id (repr_dirpath dir) in + make_dirpath (List.map id_of_string (s :: List.tl l)) + in + let l = List.map string_of_id (repr_dirpath fulldir) in + if l = [ "List"; "Lists"; "Coq" ] then update "MonoList" + else if l = [ "PolyList"; "Lists"; "Coq" ] then update "List" + else dir + else dir + +let shortest_qualid_of_v7_global ctx ref = + let fulldir,_ = repr_path (sp_of_global ref) in + let dir,id = repr_qualid (shortest_qualid_of_global ctx ref) in + let dir',id = v7_to_v8_dir_id fulldir id in + let dir'' = + if dir' = [] then + (* A name that is not renamed *) + if dir = empty_dirpath & is_new_name (string_of_id id) + then + (* An unqualified name that is not renamed but which coincides *) + (* with a new name: force qualification unless it is a variable *) + if fulldir <> empty_dirpath & not (is_coq_root fulldir) + then make_dirpath [List.hd (repr_dirpath fulldir)] + else empty_dirpath + else v7_to_v8_dir fulldir dir + else + (* A stdlib name that has been renamed *) + try + let d,_ = repr_path (Nametab.full_name_cci (make_short_qualid id)) in + if not (is_coq_root d) then + (* The user has defined id, then we qualify the new name *) + v7_to_v8_dir fulldir (make_dirpath (List.map id_of_string dir')) + else empty_dirpath + with Not_found -> v7_to_v8_dir fulldir dir in + make_qualid dir'' id + +let extern_reference loc vars r = + try Qualid (loc,shortest_qualid_of_v7_global vars r) + with Not_found -> + (* happens in debugger *) + Ident (loc,id_of_string (raw_string_of_ref r)) + +(************************************************************************) +(* Equality up to location (useful for translator v8) *) + +let rec check_same_pattern p1 p2 = + match p1, p2 with + | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 -> + check_same_pattern a1 a2 + | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 -> + List.iter2 check_same_pattern a1 a2 + | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> () + | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> () + | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 -> + check_same_pattern e1 e2 + | _ -> failwith "not same pattern" + +let check_same_ref r1 r2 = + match r1,r2 with + | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> () + | Ident(_,i1), Ident(_,i2) when i1=i2 -> () + | _ -> failwith "not same ref" + +let rec check_same_type ty1 ty2 = + match ty1, ty2 with + | CRef r1, CRef r2 -> check_same_ref r1 r2 + | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 -> + List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) -> + if id1<>id2 || i1<>i2 then failwith "not same fix"; + check_same_fix_binder bl1 bl2; + check_same_type a1 a2; + check_same_type b1 b2) + fl1 fl2 + | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 -> + List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) -> + if id1<>id2 then failwith "not same fix"; + check_same_fix_binder bl1 bl2; + check_same_type a1 a2; + check_same_type b1 b2) + fl1 fl2 + | CArrow(_,a1,b1), CArrow(_,a2,b2) -> + check_same_type a1 a2; + check_same_type b1 b2 + | CProdN(_,bl1,a1), CProdN(_,bl2,a2) -> + List.iter2 check_same_binder bl1 bl2; + check_same_type a1 a2 + | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> + List.iter2 check_same_binder bl1 bl2; + check_same_type a1 a2 + | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 -> + check_same_type a1 a2; + check_same_type b1 b2 + | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 -> + List.iter2 check_same_type al1 al2 + | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) -> + check_same_type e1 e2; + List.iter2 (fun (a1,e1) (a2,e2) -> + if e1<>e2 then failwith "not same expl"; + check_same_type a1 a2) al1 al2 + | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) -> + List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; + List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> + List.iter2 check_same_pattern pl1 pl2; + check_same_type r1 r2) brl1 brl2 + | COrderedCase(_,_,_,a1,bl1), COrderedCase(_,_,_,a2,bl2) -> + check_same_type a1 a2; + List.iter2 check_same_type bl1 bl2 + | CHole _, CHole _ -> () + | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () + | CSort(_,s1), CSort(_,s2) when s1=s2 -> () + | CCast(_,a1,b1), CCast(_,a2,b2) -> + check_same_type a1 a2; + check_same_type b1 b2 + | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 -> + List.iter2 check_same_type e1 e2 + | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> () + | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 -> + check_same_type e1 e2 + | _ when ty1=ty2 -> () + | _ -> failwith "not same type" + +and check_same_binder (nal1,e1) (nal2,e2) = + List.iter2 (fun (_,na1) (_,na2) -> + if na1<>na2 then failwith "not same name") nal1 nal2; + check_same_type e1 e2 + +and check_same_fix_binder bl1 bl2 = + List.iter2 (fun b1 b2 -> + match b1,b2 with + LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) -> + check_same_binder (nal1,ty1) (nal2,ty2) + | LocalRawDef(na1,def1), LocalRawDef(na2,def2) -> + check_same_binder ([na1],def1) ([na2],def2) + | _ -> failwith "not same binder") bl1 bl2 + +let same c d = try check_same_type c d; true with _ -> false + +(* Idem for rawconstr *) +let option_iter2 f o1 o2 = + match o1, o2 with + Some o1, Some o2 -> f o1 o2 + | None, None -> () + | _ -> failwith "option" + +let array_iter2 f v1 v2 = + List.iter2 f (Array.to_list v1) (Array.to_list v2) + +let rec same_patt p1 p2 = + match p1, p2 with + PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar" + | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) -> + if c1<>c2 || al1 <> al2 then failwith "PatCstr"; + List.iter2 same_patt pl1 pl2 + | _ -> failwith "same_patt" + +let rec same_raw c d = + match c,d with + | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef" + | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar" + | REvar(_,e1,a1), REvar(_,e2,a2) -> + if e1 <> e2 then failwith "REvar"; + option_iter2(List.iter2 same_raw) a1 a2 + | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar" + | RApp(_,f1,a1), RApp(_,f2,a2) -> + List.iter2 same_raw (f1::a1) (f2::a2) + | RLambda(_,na1,t1,m1), RLambda(_,na2,t2,m2) -> + if na1 <> na2 then failwith "RLambda"; + same_raw t1 t2; same_raw m1 m2 + | RProd(_,na1,t1,m1), RProd(_,na2,t2,m2) -> + if na1 <> na2 then failwith "RProd"; + same_raw t1 t2; same_raw m1 m2 + | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) -> + if na1 <> na2 then failwith "RLetIn"; + same_raw t1 t2; same_raw m1 m2 + | RCases(_,_,c1,b1), RCases(_,_,c2,b2) -> + List.iter2 + (fun (t1,{contents=(al1,oind1)}) (t2,{contents=(al2,oind2)}) -> + same_raw t1 t2; + if al1 <> al2 then failwith "RCases"; + option_iter2(fun (_,i1,nl1) (_,i2,nl2) -> + if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2; + List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) -> + List.iter2 same_patt pl1 pl2; + same_raw b1 b2) b1 b2 + | ROrderedCase(_,_,_,c1,v1,_), ROrderedCase(_,_,_,c2,v2,_) -> + same_raw c1 c2; + array_iter2 same_raw v1 v2 + | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) -> + if nl1<>nl2 then failwith "RLetTuple"; + same_raw b1 b2; + same_raw c1 c2 + | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) -> + same_raw b1 b2; same_raw t1 t2; same_raw e1 e2 + | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) -> + if fk1 <> fk2 || na1 <> na2 then failwith "RRec"; + array_iter2 + (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) -> + if na1<>na2 then failwith "RRec"; + option_iter2 same_raw bd1 bd2; + same_raw ty1 ty2)) bl1 bl2; + array_iter2 same_raw ty1 ty2; + array_iter2 same_raw def1 def2 + | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort" + | RHole _, _ -> () + | _, RHole _ -> () + | RCast(_,c1,_),r2 -> same_raw c1 r2 + | r1, RCast(_,c2,_) -> same_raw r1 c2 + | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic" + | _ -> failwith "same_raw" + +let same_rawconstr c d = + try same_raw c d; true + with Failure _ | Invalid_argument _ -> false + +(**********************************************************************) +(* mapping patterns to cases_pattern_expr *) + +let make_current_scopes (scopt,scopes) = + option_fold_right push_scope scopt scopes + +let has_curly_brackets ntn = + String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or + String.sub ntn (String.length ntn - 6) 6 = " { _ }" or + string_string_contains ntn " { _ } ") + +let rec wildcards ntn n = + if n = String.length ntn then [] + else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l +and spaces ntn n = + if n = String.length ntn then [] + else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1) + +let expand_curly_brackets make_ntn ntn l = + let ntn' = ref ntn in + let rec expand_ntn i = + function + | [] -> [] + | a::l -> + let a' = + let p = List.nth (wildcards !ntn' 0) i - 2 in + if p>=0 & p+5 <= String.length !ntn' & String.sub !ntn' p 5 = "{ _ }" + then begin + ntn' := + String.sub !ntn' 0 p ^ "_" ^ + String.sub !ntn' (p+5) (String.length !ntn' -p-5); + make_ntn "{ _ }" [a] end + else a in + a' :: expand_ntn (i+1) l in + let l = expand_ntn 0 l in + (* side effect *) + make_ntn !ntn' l + +let make_notation loc ntn l = + if has_curly_brackets ntn + then expand_curly_brackets (fun n l -> CNotation (loc,n,l)) ntn l + else match ntn,l with + (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) + | "- _", [CNumeral(_,Bignat.POS p)] -> + CNotation (loc,ntn,[CNotation(loc,"( _ )",l)]) + | _ -> CNotation (loc,ntn,l) + +let make_pat_notation loc ntn l = + if has_curly_brackets ntn + then expand_curly_brackets (fun n l -> CPatNotation (loc,n,l)) ntn l + else match ntn,l with + (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) + | "- _", [CPatNumeral(_,Bignat.POS p)] -> + CPatNotation (loc,ntn,[CPatNotation(loc,"( _ )",l)]) + | _ -> CPatNotation (loc,ntn,l) + + +(* +let rec cases_pattern_expr_of_constr_expr = function + | CRef r -> CPatAtom (dummy_loc,Some r) + | CHole loc -> CPatAtom (loc,None) + | CApp (loc,(proj,CRef c),l) when proj = None -> + let l,e = List.split l in + if not (List.for_all ((=) None) e) then + anomaly "Unexpected explicitation in pattern"; + CPatCstr (loc,c,List.map cases_pattern_expr_of_constr_expr l) + | CNotation (loc,ntn,l) -> + CPatNotation (loc,ntn,List.map cases_pattern_expr_of_constr_expr l) + | CNumeral (loc,n) -> CPatNumeral (loc,n) + | CDelimiters (loc,s,e) -> + CPatDelimiters (loc,s,cases_pattern_expr_of_constr_expr e) + | _ -> anomaly "Constrextern: not a pattern" + +let rec rawconstr_of_cases_pattern = function + | PatVar (loc,Name id) -> RVar (loc,id) + | PatVar (loc,Anonymous) -> RHole (loc,InternalHole) + | PatCstr (loc,(ind,_ as c),args,_) -> + let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in + let params = list_tabulate (fun _ -> RHole (loc,InternalHole)) nparams in + let args = params @ List.map rawconstr_of_cases_pattern args in + let f = RRef (loc,ConstructRef c) in + if args = [] then f else RApp (loc,f,args) +*) + +let bind_env sigma var v = + try + let vvar = List.assoc var sigma in + if v=vvar then sigma else raise No_match + with Not_found -> + (* TODO: handle the case of multiple occs in different scopes *) + (var,v)::sigma + +let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with + | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1 + | PatVar (_,Anonymous), AHole _ -> sigma + | a, AHole _ when not(Options.do_translate()) -> sigma + | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ -> + let nparams = + (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in + let l2 = + match a2 with + | ARef (ConstructRef r2) when r1 = r2 -> [] + | AApp (ARef (ConstructRef r2),l2) when r1 = r2 -> l2 + | _ -> raise No_match in + if List.length l2 <> nparams + List.length args1 + then raise No_match + else + let (p2,args2) = list_chop nparams l2 in + (* All parameters must be _ *) + List.iter (function AHole _ -> () | _ -> raise No_match) p2; + List.fold_left2 (match_cases_pattern metas) sigma args1 args2 + | _ -> raise No_match + +let match_aconstr_cases_pattern c (metas_scl,pat) = + let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in + (* Reorder canonically the substitution *) + let find x subst = + try List.assoc x subst + with Not_found -> anomaly "match_aconstr_cases_pattern" in + List.map (fun (x,scl) -> (find x subst,scl)) metas_scl + + (* Better to use extern_rawconstr composed with injection/retraction ?? *) +let rec extern_cases_pattern_in_scope scopes vars pat = + try + if !Options.raw_print or !print_no_symbol then raise No_match; + let (sc,n) = Symbols.uninterp_cases_numeral pat in + match Symbols.availability_of_numeral sc (make_current_scopes scopes) with + | None -> raise No_match + | Some key -> + let loc = pattern_loc pat in + insert_pat_delimiters (CPatNumeral (loc,n)) key + with No_match -> + try + if !Options.raw_print or !print_no_symbol then raise No_match; + extern_symbol_pattern scopes vars pat + (Symbols.uninterp_cases_pattern_notations pat) + with No_match -> + match pat with + | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,v7_to_v8_id id))) + | PatVar (loc,Anonymous) -> CPatAtom (loc, None) + | PatCstr(loc,cstrsp,args,na) -> + let args = List.map (extern_cases_pattern_in_scope scopes vars) args in + let p = CPatCstr + (loc,extern_reference loc vars (ConstructRef cstrsp),args) in + (match na with + | Name id -> CPatAlias (loc,p,v7_to_v8_id id) + | Anonymous -> p) + +and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function + | [] -> raise No_match + | (keyrule,pat,n as rule)::rules -> + try + (* Check the number of arguments expected by the notation *) + let loc = match t,n with + | PatCstr (_,f,l,_), Some n when List.length l > n -> + raise No_match + | PatCstr (loc,_,_,_),_ -> loc + | PatVar (loc,_),_ -> loc in + (* Try matching ... *) + let subst = match_aconstr_cases_pattern t pat in + (* Try availability of interpretation ... *) + match keyrule with + | NotationRule (sc,ntn) -> + let scopes' = make_current_scopes (tmp_scope, scopes) in + (match Symbols.availability_of_notation (sc,ntn) scopes' with + (* Uninterpretation is not allowed in current context *) + | None -> raise No_match + (* Uninterpretation is allowed in current context *) + | Some (scopt,key) -> + let scopes = make_current_scopes (scopt, scopes) in + let l = + List.map (fun (c,(scopt,scl)) -> + extern_cases_pattern_in_scope + (scopt,List.fold_right push_scope scl scopes) vars c) + subst in + insert_pat_delimiters (make_pat_notation loc ntn l) key) + | SynDefRule kn -> + CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn))) + with + No_match -> extern_symbol_pattern allscopes vars t rules + +(**********************************************************************) +(* Externalising applications *) + +let occur_name na aty = + match na with + | Name id -> occur_var_constr_expr id aty + | Anonymous -> false + +let is_projection nargs = function + | Some r when not !Options.raw_print & !print_projections -> + (try + let n = Recordops.find_projection_nparams r + 1 in + if n <= nargs then Some n else None + with Not_found -> None) + | _ -> None + +let is_nil = function + | [CRef ref] -> snd (repr_qualid (snd (qualid_of_reference ref))) = id_of_string "nil" + | _ -> false + +let stdlib_but_length args = function + | Some r -> + let dir,id = repr_path (sp_of_global r) in + (is_coq_root (Lib.library_dp()) or is_coq_root dir) + && not (List.mem (string_of_id id) ["Zlength";"length"] && is_nil args) + && not (List.mem (string_of_id id) ["In"] && List.length args >= 2 + && is_nil (List.tl args)) + | None -> false + +let explicit_code imp q = + dummy_loc, + if !Options.v7 & not (Options.do_translate()) then ExplByPos q + else ExplByName (name_of_implicit imp) + +let is_hole = function CHole _ -> true | _ -> false + +let is_significant_implicit a impl tail = + not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl)) + +(* Implicit args indexes are in ascending order *) +(* inctx is useful only if there is a last argument to be deduced from ctxt *) +let explicitize loc inctx impl (cf,f) args = + let n = List.length args in + let rec exprec q = function + | a::args, imp::impl when is_status_implicit imp -> + let tail = exprec (q+1) (args,impl) in + let visible = + !Options.raw_print or + (!print_implicits & !print_implicits_explicit_args) or + (is_significant_implicit a impl tail & + (not (is_inferable_implicit inctx n imp) or + (Options.do_translate() & not (stdlib_but_length args cf)))) + in + if visible then (a,Some (explicit_code imp q)) :: tail else tail + | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) + | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) + | [], _ -> [] in + match is_projection (List.length args) cf with + | Some i as ip -> + if impl <> [] & is_status_implicit (List.nth impl (i-1)) then + let f' = match f with CRef f -> f | _ -> assert false in + CAppExpl (loc,(ip,f'),args) + else + let (args1,args2) = list_chop i args in + let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in + let args1 = exprec 1 (args1,impl1) in + let args2 = exprec (i+1) (args2,impl2) in + CApp (loc,(Some (List.length args1),f),args1@args2) + | None -> + let args = exprec 1 (args,impl) in + if args = [] then f else CApp (loc, (None, f), args) + +let extern_global loc impl f = + if impl <> [] & List.for_all is_status_implicit impl then + CAppExpl (loc, (None, f), []) + else + CRef f + +let extern_app loc inctx impl (cf,f) args = + if args = [] (* maybe caused by a hidden coercion *) then + extern_global loc impl f + else + if + ((!Options.raw_print or + (!print_implicits & not !print_implicits_explicit_args)) & + List.exists is_status_implicit impl) + then + CAppExpl (loc, (is_projection (List.length args) cf, f), args) + else + explicitize loc inctx impl (cf,CRef f) args + +let rec extern_args extern scopes env args subscopes = + match args with + | [] -> [] + | a::args -> + let argscopes, subscopes = match subscopes with + | [] -> (None,scopes), [] + | scopt::subscopes -> (scopt,scopes), subscopes in + extern argscopes env a :: extern_args extern scopes env args subscopes + +let rec remove_coercions inctx = function + | RApp (loc,RRef (_,r),args) as c + when + inctx & + not (!Options.raw_print or !print_coercions or Options.do_translate ()) + -> + (try match Classops.hide_coercion r with + | Some n when n < List.length args -> + (* We skip a coercion *) + let l = list_skipn n args in + let (a,l) = match l with a::l -> (a,l) | [] -> assert false in + let (a,l) = + (* Recursively remove the head coercions *) + match remove_coercions inctx a with + | RApp (_,a,l') -> a,l'@l + | a -> a,l in + if l = [] then a + else + (* Recursively remove coercions in arguments *) + RApp (loc,a,List.map (remove_coercions true) l) + | _ -> c + with Not_found -> c) + | c -> c + +let rec rename_rawconstr_var id0 id1 = function + RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1) + | RVar(loc,id) when id=id0 -> RVar(loc,id1) + | c -> map_rawconstr (rename_rawconstr_var id0 id1) c + +let rec share_fix_binders n rbl ty def = + match ty,def with + RProd(_,na0,t0,b), RLambda(_,na1,t1,m) -> + if not(same_rawconstr t0 t1) then List.rev rbl, ty, def + else + let (na,b,m) = + match na0, na1 with + Name id0, Name id1 -> + if id0=id1 then (na0,b,m) + else if not (occur_rawconstr id1 b) then + (na1,rename_rawconstr_var id0 id1 b,m) + else if not (occur_rawconstr id0 m) then + (na1,b,rename_rawconstr_var id1 id0 m) + else (* vraiment pas de chance! *) + failwith "share_fix_binders: capture" + | Name id, Anonymous -> + if not (occur_rawconstr id m) then (na0,b,m) + else + failwith "share_fix_binders: capture" + | Anonymous, Name id -> + if not (occur_rawconstr id b) then (na1,b,m) + else + failwith "share_fix_binders: capture" + | _ -> (na1,b,m) in + share_fix_binders (n-1) ((na,None,t0)::rbl) b m + | _ -> List.rev rbl, ty, def + +(**********************************************************************) +(* mapping rawterms to constr_expr *) + +let rec extern inctx scopes vars r = + try + if !Options.raw_print or !print_no_symbol then raise No_match; + extern_numeral (Rawterm.loc_of_rawconstr r) + scopes (Symbols.uninterp_numeral r) + with No_match -> + + let r = remove_coercions inctx r in + + try + if !Options.raw_print or !print_no_symbol then raise No_match; + extern_symbol scopes vars r (Symbols.uninterp_notations r) + with No_match -> match r with + | RRef (loc,ref) -> + extern_global loc (implicits_of_global_out ref) + (extern_reference loc vars ref) + + | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id)) + + | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n + + | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n) + + | RApp (loc,f,args) -> + (match f with + | RRef (rloc,ref) -> + let subscopes = Symbols.find_arguments_scope ref in + let args = + extern_args (extern true) (snd scopes) vars args subscopes in + extern_app loc inctx (implicits_of_global_out ref) + (Some ref,extern_reference rloc vars ref) + args + | RVar (rloc,id) -> (* useful for translation of inductive *) + let args = List.map (sub_extern true scopes vars) args in + extern_app loc inctx (get_temporary_implicits_out id) + (None,Ident (rloc,v7_to_v8_id id)) + args + | _ -> + explicitize loc inctx [] (None,sub_extern false scopes vars f) + (List.map (sub_extern true scopes vars) args)) + + | RProd (loc,Anonymous,t,c) -> + (* Anonymous product are never factorized *) + CArrow (loc,extern_type scopes vars t, extern_type scopes vars c) + + | RLetIn (loc,na,t,c) -> + let na = name_app translate_ident na in + CLetIn (loc,(loc,na),sub_extern false scopes vars t, + extern inctx scopes (add_vname vars na) c) + + | RProd (loc,na,t,c) -> + let t = extern_type scopes vars (anonymize_if_reserved na t) in + let (idl,c) = factorize_prod scopes (add_vname vars na) t c in + CProdN (loc,[(dummy_loc,na)::idl,t],c) + + | RLambda (loc,na,t,c) -> + let t = extern_type scopes vars (anonymize_if_reserved na t) in + let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in + CLambdaN (loc,[(dummy_loc,na)::idl,t],c) + + | RCases (loc,(typopt,rtntypopt),tml,eqns) -> + let pred = option_app (extern_type scopes vars) typopt in + let vars' = + List.fold_right (name_fold Idset.add) + (cases_predicate_names tml) vars in + let rtntypopt' = option_app (extern_type scopes vars') !rtntypopt in + let tml = List.map (fun (tm,{contents=(na,x)}) -> + let na' = match na,tm with + Anonymous, RVar (_,id) when + !rtntypopt<>None & occur_rawconstr id (out_some !rtntypopt) + -> Some Anonymous + | Anonymous, _ -> None + | Name id, RVar (_,id') when id=id' -> None + | Name _, _ -> Some na in + (sub_extern false scopes vars tm, + (na',option_app (fun (loc,ind,nal) -> + let args = List.map (function + | Anonymous -> RHole (dummy_loc,InternalHole) + | Name id -> RVar (dummy_loc,id)) nal in + let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in + (extern_type scopes vars t)) x))) tml in + let eqns = List.map (extern_eqn (typopt<>None) scopes vars) eqns in + CCases (loc,(pred,rtntypopt'),tml,eqns) + + | ROrderedCase (loc,cs,typopt,tm,bv,{contents = Some x}) -> + extern false scopes vars x + + | ROrderedCase (loc,IfStyle,typopt,tm,bv,_) when Options.do_translate () -> + let rec strip_branches = function + | (RLambda (_,_,_,c1), RLambda (_,_,_,c2)) -> strip_branches (c1,c2) + | x -> x in + let c1,c2 = strip_branches (bv.(0),bv.(1)) in + msgerrnl (str "Warning: unable to ensure the correctness of the translation of an if-then-else"); + let bv = Array.map (sub_extern (typopt<>None) scopes vars) [|c1;c2|] in + COrderedCase + (loc,IfStyle,option_app (extern_type scopes vars) typopt, + sub_extern false scopes vars tm,Array.to_list bv) + (* We failed type-checking If and to translate it to CIf *) + (* try to remove the dependances in branches anyway *) + + + | ROrderedCase (loc,cs,typopt,tm,bv,_) -> + let bv = Array.map (sub_extern (typopt<>None) scopes vars) bv in + COrderedCase + (loc,cs,option_app (extern_type scopes vars) typopt, + sub_extern false scopes vars tm,Array.to_list bv) + + | RLetTuple (loc,nal,(na,typopt),tm,b) -> + CLetTuple (loc,nal, + (Some na,option_app (extern_type scopes (add_vname vars na)) typopt), + sub_extern false scopes vars tm, + extern false scopes (List.fold_left add_vname vars nal) b) + + | RIf (loc,c,(na,typopt),b1,b2) -> + CIf (loc,sub_extern false scopes vars c, + (Some na,option_app (extern_type scopes (add_vname vars na)) typopt), + sub_extern false scopes vars b1, sub_extern false scopes vars b2) + + | RRec (loc,fk,idv,blv,tyv,bv) -> + let vars' = Array.fold_right Idset.add idv vars in + (match fk with + | RFix (nv,n) -> + let listdecl = + Array.mapi (fun i fi -> + let (bl,ty,def) = + if Options.do_translate() then + let n = List.fold_left + (fun n (_,obd,_) -> if obd=None then n-1 else n) + nv.(i) blv.(i) in + share_fix_binders n (List.rev blv.(i)) tyv.(i) bv.(i) + else blv.(i), tyv.(i), bv.(i) in + let (ids,bl) = extern_local_binder scopes vars bl in + let vars0 = List.fold_right (name_fold Idset.add) ids vars in + let vars1 = List.fold_right (name_fold Idset.add) ids vars' in + (fi,nv.(i), bl, extern_type scopes vars0 ty, + extern false scopes vars1 def)) idv + in + CFix (loc,(loc,idv.(n)),Array.to_list listdecl) + | RCoFix n -> + let listdecl = + Array.mapi (fun i fi -> + let (ids,bl) = extern_local_binder scopes vars blv.(i) in + let vars0 = List.fold_right (name_fold Idset.add) ids vars in + let vars1 = List.fold_right (name_fold Idset.add) ids vars' in + (fi,bl,extern_type scopes vars0 tyv.(i), + sub_extern false scopes vars1 bv.(i))) idv + in + CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) + + | RSort (loc,s) -> + let s = match s with + | RProp _ -> s + | RType (Some _) when !print_universes -> s + | RType _ -> RType None in + CSort (loc,s) + + | RHole (loc,e) -> CHole loc + + | RCast (loc,c,t) -> + CCast (loc,sub_extern true scopes vars c,extern_type scopes vars t) + + | RDynamic (loc,d) -> CDynamic (loc,d) + +and extern_type (_,scopes) = extern true (Some Symbols.type_scope,scopes) + +and sub_extern inctx (_,scopes) = extern inctx (None,scopes) + +and factorize_prod scopes vars aty = function + | RProd (loc,(Name id as na),ty,c) + when same aty (extern_type scopes vars (anonymize_if_reserved na ty)) + & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) + -> let id = translate_ident id in + let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in + ((loc,Name id)::nal,c) + | c -> ([],extern_type scopes vars c) + +and factorize_lambda inctx scopes vars aty = function + | RLambda (loc,na,ty,c) + when same aty (extern_type scopes vars (anonymize_if_reserved na ty)) + & not (occur_name na aty) (* To avoid na in ty' escapes scope *) + -> let na = name_app translate_ident na in + let (nal,c) = + factorize_lambda inctx scopes (add_vname vars na) aty c in + ((loc,na)::nal,c) + | c -> ([],sub_extern inctx scopes vars c) + +and extern_local_binder scopes vars = function + [] -> ([],[]) + | (na,Some bd,ty)::l -> + let na = name_app translate_ident na in + let (ids,l) = + extern_local_binder scopes (name_fold Idset.add na vars) l in + (na::ids, + LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l) + + | (na,None,ty)::l -> + let na = name_app translate_ident na in + let ty = extern_type scopes vars (anonymize_if_reserved na ty) in + (match extern_local_binder scopes (name_fold Idset.add na vars) l with + (ids,LocalRawAssum(nal,ty')::l) + when same ty ty' & + match na with Name id -> not (occur_var_constr_expr id ty') + | _ -> true -> + (na::ids, + LocalRawAssum((dummy_loc,na)::nal,ty')::l) + | (ids,l) -> + (na::ids, + LocalRawAssum([(dummy_loc,na)],ty) :: l)) + +and extern_eqn inctx scopes vars (loc,ids,pl,c) = + (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, + extern inctx scopes vars c) + +and extern_numeral loc scopes (sc,n) = + match Symbols.availability_of_numeral sc (make_current_scopes scopes) with + | None -> raise No_match + | Some key -> insert_delimiters (CNumeral (loc,n)) key + +and extern_symbol (tmp_scope,scopes as allscopes) vars t = function + | [] -> raise No_match + | (keyrule,pat,n as rule)::rules -> + let loc = Rawterm.loc_of_rawconstr t in + try + (* Adjusts to the number of arguments expected by the notation *) + let (t,args) = match t,n with + | RApp (_,f,args), Some n when List.length args > n -> + let args1, args2 = list_chop n args in + RApp (dummy_loc,f,args1), args2 + | _ -> t,[] in + (* Try matching ... *) + let subst = match_aconstr t pat in + (* Try availability of interpretation ... *) + let e = + match keyrule with + | NotationRule (sc,ntn) -> + let scopes' = make_current_scopes (tmp_scope, scopes) in + (match Symbols.availability_of_notation (sc,ntn) scopes' with + (* Uninterpretation is not allowed in current context *) + | None -> raise No_match + (* Uninterpretation is allowed in current context *) + | Some (scopt,key) -> + let scopes = make_current_scopes (scopt, scopes) in + let l = + List.map (fun (c,(scopt,scl)) -> + extern (* assuming no overloading: *) true + (scopt,List.fold_right push_scope scl scopes) vars c) + subst in + insert_delimiters (make_notation loc ntn l) key) + | SynDefRule kn -> + CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in + if args = [] then e + else + (* TODO: compute scopt for the extra args, in case, head is a ref *) + explicitize loc false [] (None,e) + (List.map (extern true allscopes vars) args) + with + No_match -> extern_symbol allscopes vars t rules + +let extern_rawconstr vars c = + extern false (None,Symbols.current_scopes()) vars c + +let extern_rawtype vars c = + extern_type (None,Symbols.current_scopes()) vars c + +let extern_cases_pattern vars p = + extern_cases_pattern_in_scope (None,Symbols.current_scopes()) vars p + +(******************************************************************) +(* Main translation function from constr -> constr_expr *) + +let loc = dummy_loc (* for constr and pattern, locations are lost *) + +let extern_constr_gen at_top scopt env t = + let vars = vars_of_env env in + let avoid = if at_top then ids_of_context env else [] in + extern (not at_top) (scopt,Symbols.current_scopes()) vars + (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t) + +let extern_constr_in_scope at_top scope env t = + extern_constr_gen at_top (Some scope) env t + +let extern_constr at_top env t = + extern_constr_gen at_top None env t + +(******************************************************************) +(* Main translation function from pattern -> constr_expr *) + +let rec raw_of_pat tenv env = function + | PRef ref -> RRef (loc,ref) + | PVar id -> RVar (loc,id) + | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat tenv env) l)) + | PRel n -> + let id = try match lookup_name_of_rel n env with + | Name id -> id + | Anonymous -> + anomaly "rawconstr_of_pattern: index to an anonymous variable" + with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in + RVar (loc,id) + | PMeta None -> RHole (loc,InternalHole) + | PMeta (Some n) -> RPatVar (loc,(false,n)) + | PApp (f,args) -> + RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args) + | PSoApp (n,args) -> + RApp (loc,RPatVar (loc,(true,n)), + List.map (raw_of_pat tenv env) args) + | PProd (na,t,c) -> + RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c) + | PLetIn (na,t,c) -> + RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) + | PLambda (na,t,c) -> + RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) + | PCase ((_,(IfStyle|LetStyle as cs)),typopt,tm,bv) -> + ROrderedCase (loc,cs,option_app (raw_of_pat tenv env) typopt, + raw_of_pat tenv env tm,Array.map (raw_of_pat tenv env) bv, ref None) + | PCase ((_,cs),typopt,tm,[||]) -> + RCases (loc,(option_app (raw_of_pat tenv env) typopt,ref None (* TODO *)), + [raw_of_pat tenv env tm,ref (Anonymous,None)],[]) + | PCase ((Some ind,cs),typopt,tm,bv) -> + let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in + let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in + Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env) + (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) + tenv avoid ind cs typopt k tm bv + | PCase _ -> error "Unsupported case-analysis while printing pattern" + | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f) + | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c) + | PSort s -> RSort (loc,s) + +and raw_of_eqn tenv env constr construct_nargs branch = + let make_pat x env b ids = + let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in + let id = next_name_away_with_default "x" x avoid in + PatVar (dummy_loc,Name id),(Name id)::env,id::ids + in + let rec buildrec ids patlist env n b = + if n=0 then + (dummy_loc, ids, + [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], + raw_of_pat tenv env b) + else + match b with + | PLambda (x,_,b) -> + let pat,new_env,new_ids = make_pat x env b ids in + buildrec new_ids (pat::patlist) new_env (n-1) b + + | PLetIn (x,_,b) -> + let pat,new_env,new_ids = make_pat x env b ids in + buildrec new_ids (pat::patlist) new_env (n-1) b + + | _ -> + error "Unsupported branch in case-analysis while printing pattern" + in + buildrec [] [] env construct_nargs branch + +let extern_pattern tenv env pat = + extern true (None,Symbols.current_scopes()) Idset.empty + (raw_of_pat tenv env pat) diff --git a/interp/constrextern.mli b/interp/constrextern.mli new file mode 100644 index 00000000..ad1c4391 --- /dev/null +++ b/interp/constrextern.mli @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + trees for printing *) + +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 + +(* 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 *) + +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 + +(* Printing options *) +val print_implicits : bool ref +val print_arguments : bool ref +val print_evar_arguments : bool ref +val print_coercions : bool ref +val print_universes : bool ref +val print_no_symbol : bool ref +val print_projections : bool ref + +(* This governs printing of implicit arguments. If [with_implicits] is + on and not [with_arguments] then implicit args are printed prefixed + by "!"; if [with_implicits] and [with_arguments] are both on the + function and not the arguments is prefixed by "!" *) +val with_implicits : ('a -> 'b) -> 'a -> 'b +val with_arguments : ('a -> 'b) -> 'a -> 'b + +(* This forces printing of coercions *) +val with_coercions : ('a -> 'b) -> 'a -> 'b + +(* This forces printing universe names of Type{.} *) +val with_universes : ('a -> 'b) -> 'a -> 'b + +(* This suppresses printing of numeral and symbols *) +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 new file mode 100644 index 00000000..e1b916e1 --- /dev/null +++ b/interp/constrintern.ml @@ -0,0 +1,1165 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 1 then "s" else "" in + str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found " + ++ int n2 + +let explain_bad_explicitation_number n po = + match n with + | ExplByPos n -> + let s = match po with + | None -> str "a regular argument" + | Some p -> int p in + str "Bad explicitation number: found " ++ int n ++ + str" but was expecting " ++ s + | ExplByName id -> + let s = match po with + | None -> str "a regular argument" + | Some p -> (*pr_id (name_of_position p) in*) failwith "" in + str "Bad explicitation name: found " ++ pr_id id ++ + str" but was expecting " ++ s + +let explain_internalisation_error = function + | VariableCapture id -> explain_variable_capture id + | WrongExplicitImplicit -> explain_wrong_explicit_implicit + | NegativeMetavariable -> explain_negative_metavariable + | NotAConstructor ref -> explain_not_a_constructor ref + | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id + | NonLinearPattern id -> explain_non_linear_pattern id + | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 + | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po + +let error_unbound_patvar loc n = + user_err_loc + (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ + str " is unbound") + +let error_bad_inductive_type loc = + user_err_loc (loc,"",str + "This should be an inductive type applied to names or \"_\"") + +(**********************************************************************) +(* Dump of globalization (to be used by coqdoc) *) +let token_number = ref 0 +let last_pos = ref 0 + +type coqdoc_state = Lexer.location_table * int * int + +let coqdoc_freeze () = + let lt = Lexer.location_table() in + let state = (lt,!token_number,!last_pos) in + token_number := 0; + last_pos := 0; + state + +let coqdoc_unfreeze (lt,tn,lp) = + Lexer.restore_location_table lt; + token_number := tn; + last_pos := lp + +let add_glob loc ref = +(*i + let sp = Nametab.sp_of_global (Global.env ()) ref in + let dir,_ = repr_path sp in + let rec find_module d = + try + let qid = let dir,id = split_dirpath d in make_qualid dir id in + let _ = Nametab.locate_loaded_library qid in d + with Not_found -> find_module (dirpath_prefix d) + in + let s = string_of_dirpath (find_module dir) in + i*) + let sp = Nametab.sp_of_global ref in + let id = let _,id = repr_path sp in string_of_id id in + 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) + else snd (unloc (f (List.hd args))) + +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) + +(**********************************************************************) +(* Contracting "{ _ }" in notations *) + +let rec wildcards ntn n = + if n = String.length ntn then [] + else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l +and spaces ntn n = + if n = String.length ntn then [] + else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1) + +let expand_notation_string ntn n = + let pos = List.nth (wildcards ntn 0) n in + let hd = if pos = 0 then "" else String.sub ntn 0 pos in + let tl = + if pos = String.length ntn then "" + else String.sub ntn (pos+1) (String.length ntn - pos -1) in + hd ^ "{ _ }" ^ tl + +(* This contracts the special case of "{ _ }" for sumbool, sumor notations *) +(* Remark: expansion of squash at definition is done in metasyntax.ml *) +let contract_notation ntn l = + let ntn' = ref ntn in + let rec contract_squash n = function + | [] -> [] + | CNotation (_,"{ _ }",[a]) :: l -> + ntn' := expand_notation_string !ntn' n; + contract_squash n (a::l) + | a :: l -> + a::contract_squash (n+1) l in + let l = contract_squash 0 l in + (* side effect; don't inline *) + !ntn',l + +let contract_pat_notation ntn l = + let ntn' = ref ntn in + let rec contract_squash n = function + | [] -> [] + | CPatNotation (_,"{ _ }",[a]) :: l -> + ntn' := expand_notation_string !ntn' n; + contract_squash n (a::l) + | a :: l -> + a::contract_squash (n+1) l in + let l = contract_squash 0 l in + (* side effect; don't inline *) + !ntn',l + +(**********************************************************************) +(* Remembering the parsing scope of variables in notations *) + +let make_current_scope (scopt,scopes) = option_cons scopt scopes + +let set_var_scope loc id (_,scopt,scopes) varscopes = + let idscopes = List.assoc id varscopes in + if !idscopes <> None & + make_current_scope (out_some !idscopes) + <> make_current_scope (scopt,scopes) then + user_err_loc (loc,"set_var_scope", + pr_id id ++ str " already occurs in a different scope") + else + idscopes := Some (scopt,scopes) + +(**********************************************************************) +(* Discriminating between bound variables and global references *) + +(* [vars1] is a set of name to avoid (used for the tactic language); + [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 (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) + 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 + then + RVar (loc,id), [], [], [] + (* Is [id] a notation variable *) + else if List.mem_assoc id vars3 + then + (set_var_scope loc id genv vars3; RVar (loc,id), [], [], []) + else + + (* Is [id] bound to a free name in ltac (this is an ltac error message) *) + try + match List.assoc id unbndltacvars with + | None -> user_err_loc (loc,"intern_var", + pr_id id ++ str " ist not 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 *) + let _ = Sign.lookup_named id vars2 in + try + (* [id] a section variable *) + (* Redundant: could be done in intern_qualid *) + let ref = VarRef id in + RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, [] + with _ -> + (* [id] a goal variable *) + RVar (loc,id), [], [], [] + +let find_appl_head_data (_,_,_,_,impls) = function + | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] + | x -> x,[],[],[] + +(* Is it a global reference or a syntactic definition? *) +let intern_qualid loc qid = + try match Nametab.extended_locate qid with + | TrueGlobal ref -> + if !dump then add_glob loc ref; + RRef (loc, ref) + | SyntacticDef sp -> + Syntax_def.search_syntactic_definition loc sp + with Not_found -> + error_global_not_found_loc loc qid + +let intern_inductive r = + let loc,qid = qualid_of_reference r in + try match Nametab.extended_locate qid with + | TrueGlobal (IndRef ind) -> ind, [] + | TrueGlobal _ -> raise Not_found + | SyntacticDef sp -> + (match Syntax_def.search_syntactic_definition loc sp with + | RApp (_,RRef(_,IndRef ind),l) + when List.for_all (function RHole _ -> true | _ -> false) l -> + (ind, List.map (fun _ -> Anonymous) l) + | _ -> raise Not_found) + with Not_found -> + error_global_not_found_loc loc qid + +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)) + with e -> + (* Extra allowance for non globalizing functions *) + if !interning_grammar then RVar (loc,id), [], [], [] + else raise e + +let interp_reference vars r = + let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r + in r + +let apply_scope_env (ids,_,scopes as env) = function + | [] -> (ids,None,scopes), [] + | sc::scl -> (ids,sc,scopes), scl + +let rec adjust_scopes env scopes = function + | [] -> [] + | a::args -> + let (enva,scopes) = apply_scope_env env scopes in + enva :: adjust_scopes env scopes args + +let rec simple_adjust_scopes = function + | _,[] -> [] + | [],_::args -> None :: simple_adjust_scopes ([],args) + | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args) + +(**********************************************************************) +(* Cases *) + +(* Check linearity of pattern-matching *) +let rec has_duplicate = function + | [] -> None + | x::l -> if List.mem x l then (Some x) else has_duplicate l + +let loc_of_lhs lhs = + join_loc (cases_pattern_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs)) + +let check_linearity lhs ids = + match has_duplicate ids with + | Some id -> + raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id)) + | 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))) + +(* 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 = + ids@[id], if ids=[] then subst else (id, List.hd ids)::subst + +let alias_of = function + | ([],_) -> Anonymous + | (id::_,_) -> Name id + +let message_redundant_alias (id1,id2) = + if_verbose warning + ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2)) + +(* Expanding notations *) + +let decode_patlist_value = function + | CPatCstr (_,_,l) -> l + | _ -> anomaly "Ill-formed list argument of notation" + +let rec subst_pat_iterator y t = function + | PatVar (_,id) as x -> + if id = Name y then t else x + | PatCstr (loc,id,l,alias) -> + PatCstr (loc,id,List.map (subst_pat_iterator y t) l,alias) + +let subst_cases_pattern loc aliases intern subst scopes a = + let rec aux aliases subst = function + | AVar id -> + begin + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) + try + 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 + anomaly ("Unbound pattern notation variable: "^(string_of_id id)) + (* + (* Happens for local notation joint with inductive/fixpoint defs *) + if aliases <> ([],[]) then + anomaly "Pattern notation without constructors"; + [[id],[]], PatVar (loc,Name id) + *) + end + | ARef (ConstructRef c) -> + [aliases], 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 _,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) + | 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 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 + with Not_found -> + anomaly "Inconsistent substitution of recursive notation") + | t -> user_err_loc (loc,"",str "Invalid notation for pattern") + in aux aliases subst a + +(* Differentiating between constructors and matching variables *) +type pattern_qualid_kind = + | ConstrPat of (constructor * cases_pattern list) + | VarPat of identifier + +let rec patt_of_rawterm loc cstr = + match cstr with + | RRef (_,(ConstructRef c as x)) -> + if !dump then add_glob loc x; + (c,[]) + | 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 npar = mib.Declarations.mind_nparams in + let (params,args) = + if List.length pl <= npar then (pl,[]) else + list_chop npar pl in + (* All parameters must be _ *) + List.iter + (function RHole _ -> () + | _ -> raise Not_found) params; + let pl' = List.map + (fun c -> + let (c,pl) = patt_of_rawterm loc c in + PatCstr(loc,c,pl,Anonymous)) args in + (c,pl') + | _ -> raise Not_found + +let find_constructor ref = + let (loc,qid) = qualid_of_reference ref in + let gref = + try extended_locate qid + with Not_found -> + raise (InternalisationError (loc,NotAConstructor ref)) in + match gref with + | SyntacticDef sp -> + let sdef = Syntax_def.search_syntactic_definition loc sp in + patt_of_rawterm loc sdef + | TrueGlobal r -> + let rec unf = function + | ConstRef cst -> + let v = Environ.constant_value (Global.env()) cst in + unf (reference_of_constr v) + | ConstructRef c -> + if !dump then add_glob loc r; + c, [] + | _ -> raise Not_found + in unf r + +let find_pattern_variable = function + | Ident (loc,id) -> id + | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x)) + +let maybe_constructor ref = + try ConstrPat (find_constructor ref) + with + (* patt var does not exists globally *) + | 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 ++ + str " is understood as a pattern variable"); + VarPat (find_pattern_variable ref) + +let mustbe_constructor loc ref = + try find_constructor ref + with (Environ.NotEvaluableConst _ | Not_found) -> + raise (InternalisationError (loc,NotAConstructor ref)) + +let rec intern_cases_pattern scopes aliases tmp_scope = function + | CPatAlias (loc, p, id) -> + let aliases' = merge_aliases aliases id in + intern_cases_pattern 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) + | CPatNotation (_,"( _ )",[a]) -> + intern_cases_pattern 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 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) -> + let scopes = option_cons tmp_scope scopes in + ([aliases], + Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes) + | CPatDelimiters (loc, key, e) -> + intern_cases_pattern (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)) + | VarPat id -> + let aliases = merge_aliases aliases id in + ([aliases], PatVar (loc,alias_of aliases))) + | CPatAtom (loc, None) -> + ([aliases], PatVar (loc,alias_of aliases)) + +(**********************************************************************) +(* Fix and CoFix *) + +(**********************************************************************) +(* Utilities for binders *) + +let check_capture loc ty = function + | Name id when occur_var_constr_expr id ty -> + raise (InternalisationError (loc,VariableCapture id)) + | _ -> + () + +let locate_if_isevar loc na = function + | RHole _ -> + (try match na with + | Name id -> Reserve.find_reserved_type id + | Anonymous -> raise Not_found + with Not_found -> RHole (loc, BinderType na)) + | x -> x + +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 \ +of its constructor") + +let push_name_env lvar (ids,tmpsc,scopes as env) = function + | Anonymous -> env + | Name id -> + check_hidden_implicit_parameters id lvar; + (Idset.add id ids,tmpsc,scopes) + +(**********************************************************************) +(* Utilities for application *) + +let merge_impargs l args = + List.fold_right (fun a l -> + match a with + | (_,Some (_,(ExplByName id as x))) when + List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l + | _ -> a::l) + l args + +let check_projection isproj nargs r = + match (r,isproj) with + | RRef (loc, ref), Some nth -> + (try + let n = Recordops.find_projection_nparams ref in + if nargs < nth then + user_err_loc (loc,"",str "Projection has not enough parameters"); + with Not_found -> + user_err_loc + (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection")) + | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection") + | _, None -> () + +let set_hole_implicit i = function + | RRef (loc,r) -> (loc,ImplicitArg (r,i)) + | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i)) + | _ -> anomaly "Only refs have implicits" + +let exists_implicit_name id = + List.exists (fun imp -> is_status_implicit imp & id = name_of_implicit imp) + +let extract_explicit_arg imps args = + let rec aux = function + | [] -> [],[] + | (a,e)::l -> + let (eargs,rargs) = aux l in + match e with + | None -> (eargs,a::rargs) + | Some (loc,pos) -> + let id = match pos with + | ExplByName id -> + if not (exists_implicit_name id imps) then + user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id); + if List.mem_assoc id eargs then + user_err_loc (loc,"",str "Argument name " ++ pr_id id + ++ str " occurs more than once"); + id + | ExplByPos p -> + let id = + try + let imp = List.nth imps (p-1) in + if not (is_status_implicit imp) then failwith "imp"; + name_of_implicit imp + with Failure _ (* "nth" | "imp" *) -> + user_err_loc (loc,"",str"Wrong argument position: " ++ int p) + in + if List.mem_assoc id eargs then + user_err_loc (loc,"",str"Argument at position " ++ int p ++ + str " is mentioned more than once"); + id in + ((id,(loc,a))::eargs,rargs) + in aux 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) = + let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in + id,(Idset.add id ids,tmpsc,scopes) + +let decode_constrlist_value = function + | CAppExpl (_,_,l) -> l + | _ -> anomaly "Ill-formed list argument of notation" + +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) = + function + | AVar id -> + begin + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) + try + let (a,(scopt,subscopes)) = List.assoc id subst in + interp (ids,scopt,subscopes@scopes) a + with Not_found -> + (* Happens for local notation joint with inductive/fixpoint defs *) + RVar (loc,id) + end + | 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 termin = + subst_aconstr_in_rawconstr loc interp subst (ids,None,scopes) + terminator in + let l = decode_constrlist_value a in + List.fold_right (fun a t -> + subst_iterator ldots_var t + (subst_aconstr_in_rawconstr loc interp + ((x,(a,(scopt,subscopes)))::subst) + (ids,None,scopes) iter)) + (if lassoc then List.rev l else l) termin + with Not_found -> + anomaly "Inconsistent substitution of recursive notation") + | t -> + rawconstr_of_aconstr_with_binders loc (traverse_binder subst) + (subst_aconstr_in_rawconstr loc interp subst) (ids,None,scopes) t + +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 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) + +let reset_tmp_scope (ids,tmp_scope,scopes) = + (ids,None,scopes) + +(**********************************************************************) +(* Main loop *) + +let internalise sigma 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 + (match intern_impargs c env imp subscopes l with + | [] -> c + | l -> RApp (constr_loc x, c, l)) + | CFix (loc, (locid,iddef), dl) -> + let lf = List.map (fun (id,_,_,_,_) -> id) dl in + let dl = Array.of_list dl in + let n = + try + (list_index iddef lf) -1 + 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), + Array.of_list lf, + 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 + let n = + try + (list_index iddef lf) -1 + 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) = + 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,RCoFix n, + Array.of_list lf, + Array.map (fun (bl,_,_) -> bl) idl, + Array.map (fun (_,ty,_) -> ty) idl, + Array.map (fun (_,_,bd) -> bd) idl) + | CArrow (loc,c1,c2) -> + RProd (loc, Anonymous, intern_type env c1, intern_type env c2) + | CProdN (loc,[],c2) -> + intern_type env c2 + | CProdN (loc,(nal,ty)::bll,c2) -> + iterate_prod loc env ty (CProdN (loc, bll, c2)) nal + | CLambdaN (loc,[],c2) -> + intern env c2 + | CLambdaN (loc,(nal,ty)::bll,c2) -> + iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal + | 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 (_,"( _ )",[a]) -> intern env a + | CNotation (loc,ntn,args) -> + intern_notation intern env loc ntn args + | CNumeral (loc, n) -> + let scopes = option_cons tmp_scope scopes in + Symbols.interp_numeral loc n scopes + | CDelimiters (loc, key, e) -> + intern (ids,None,find_delimiters_scope loc key::scopes) e + | CAppExpl (loc, (isproj,ref), args) -> + let (f,_,args_scopes,_) = intern_reference env lvar ref in + check_projection isproj (List.length args) f; + RApp (loc, f, intern_args env args_scopes args) + | CApp (loc, (isproj,f), args) -> + let isproj,f,args = match f with + (* Compact notations like "t.(f args') args" *) + | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args + (* Don't compact "(f args') args" to resolve implicits separately *) + | _ -> isproj,f,args in + let (c,impargs,args_scopes,l) = + match f with + | CRef ref -> intern_reference env lvar ref + | CNotation (loc,ntn,[]) -> + 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 + 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) -> + 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) + 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) + | 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 + let env'' = List.fold_left (push_name_env lvar) env ids in + let p' = option_app (intern_type env'') po in + RLetTuple (loc, nal, (na', p'), b', + intern (List.fold_left (push_name_env lvar) env nal) c) + | CIf (loc, c, (na,po), b1, b2) -> + let env' = reset_tmp_scope env in + let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in + let env'' = List.fold_left (push_name_env lvar) env ids in + 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) + | 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, _) -> + 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) + + | CDynamic (loc,d) -> RDynamic (loc,d) + + and intern_type (ids,_,scopes) = + intern (ids,Some Symbols.type_scope,scopes) + + and intern_local_binder ((ids,ts,sc as env),bl) = function + LocalRawAssum(nal,ty) -> + let ty = 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) + + and intern_case_item (vars,_,scopes as env) (tm,(na,t)) = + let tm' = intern env tm in + let ids,typ = match t with + | Some t -> + 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,[]) + | 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 + | None -> + [], None in + let na = match tm', na with + | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id + | _, None -> Anonymous + | _, Some na -> na in + (tm',(na,typ)), na::ids + + and iterate_prod loc2 env ty body = function + | (loc1,na)::nal -> + if nal <> [] then check_capture loc1 ty na; + let body = iterate_prod loc2 (push_name_env lvar env na) ty body nal in + let ty = locate_if_isevar loc1 na (intern_type env ty) in + RProd (join_loc loc1 loc2, na, ty, body) + | [] -> intern_type env body + + and iterate_lam loc2 env ty body = function + | (loc1,na)::nal -> + if nal <> [] then check_capture loc1 ty na; + let body = iterate_lam loc2 (push_name_env lvar env na) ty body nal in + let ty = locate_if_isevar loc1 na (intern_type env ty) in + RLambda (join_loc loc1 loc2, na, ty, body) + | [] -> intern env body + + and intern_impargs c env l subscopes args = + let eargs, rargs = extract_explicit_arg l args in + let rec aux n impl subscopes eargs rargs = + let (enva,subscopes') = apply_scope_env env subscopes in + match (impl,rargs) with + | (imp::impl', rargs) when is_status_implicit imp -> + begin try + let id = name_of_implicit imp in + let (_,a) = List.assoc id eargs in + let eargs' = List.remove_assoc id eargs in + intern enva a :: aux (n+1) impl' subscopes' eargs' rargs + with Not_found -> + if rargs=[] & eargs=[] & + not (List.for_all is_status_implicit impl') then + (* Less regular arguments than expected: don't complete *) + (* with implicit arguments *) + [] + else + RHole (set_hole_implicit n c) :: + aux (n+1) impl' subscopes' eargs rargs + end + | (imp::impl', a::rargs') -> + intern enva a :: aux (n+1) impl' subscopes' eargs rargs' + | (imp::impl', []) -> + if eargs <> [] then + (let (id,(loc,_)) = List.hd eargs in + user_err_loc (loc,"",str "Not enough non implicit + arguments to accept the argument bound to " ++ pr_id id)); + [] + | ([], rargs) -> + assert (eargs = []); + intern_args env subscopes rargs + in aux 1 l subscopes eargs rargs + + and intern_args env subscopes = function + | [] -> [] + | a::args -> + let (enva,subscopes) = apply_scope_env env subscopes in + (intern enva a) :: (intern_args env subscopes args) + + in + try + intern env c + with + InternalisationError (loc,e) -> + user_err_loc (loc,"internalize",explain_internalisation_error e) + +(**************************************************************************) +(* Functions to translate constr_expr into rawconstr *) +(**************************************************************************) + +let extract_ids env = + List.fold_right Idset.add + (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 interp_rawtype_with_implicits sigma env impls c = + interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) 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 +*) + +(*********************************************************************) +(* 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 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 + +(* 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 + +(*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 c typ = + understand_gen sigma env [] (Some typ) (interp_rawconstr 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_constrpattern_gen sigma env ltacvar c = + let c = interp_rawconstr_gen false sigma env true (ltacvar,[]) c in + pattern_of_rawconstr c + +let interp_constrpattern sigma env c = + interp_constrpattern_gen sigma env [] 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 + (* 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 *) + (* Variables occurring in binders have no relevant scope since bound *) + List.map + (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl, + a + +(**********************************************************************) +(* Locating reference, possibly via an abbreviation *) + +let locate_reference qid = + match Nametab.extended_locate qid with + | TrueGlobal ref -> ref + | SyntacticDef kn -> + match Syntax_def.search_syntactic_definition dummy_loc kn with + | Rawterm.RRef (_,ref) -> ref + | _ -> raise Not_found + +let is_global id = + try + let _ = locate_reference (make_short_qualid id) in true + with Not_found -> + false + +let global_reference id = + constr_of_reference (locate_reference (make_short_qualid id)) + +let construct_reference ctx id = + try + Term.mkVar (let _ = Sign.lookup_named id ctx in id) + with Not_found -> + global_reference id + +let global_reference_in_absolute_module dir id = + constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id)) + diff --git a/interp/constrintern.mli b/interp/constrintern.mli new file mode 100644 index 00000000..a65ab6a7 --- /dev/null +++ b/interp/constrintern.mli @@ -0,0 +1,126 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + +val interp_constrpattern : + evar_map -> env -> constr_expr -> patvar list * constr_pattern + +val interp_reference : ltac_sign -> reference -> rawconstr + +(* Locating references of constructions, possibly via a syntactic definition *) + +val locate_reference : qualid -> global_reference +val is_global : identifier -> bool +val construct_reference : named_context -> identifier -> constr +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 + +(* Globalization leak for Grammar *) +val for_grammar : ('a -> 'b) -> 'a -> 'b + +(* Coqdoc utility functions *) +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 new file mode 100644 index 00000000..8ce9bfaf --- /dev/null +++ b/interp/coqlib.ml @@ -0,0 +1,294 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + anomaly (locstr^": cannot find "^(string_of_path sp)) + +let gen_constant locstr dir s = + constr_of_reference (gen_reference locstr dir s) + +let list_try_find f = + let rec try_find_f = function + | [] -> raise Not_found + | h::t -> try f h with Not_found -> try_find_f t + in + try_find_f + +let has_suffix_in_dirs dirs ref = + let dir = dirpath (sp_of_global ref) in + List.exists (fun d -> is_dirpath_prefix_of d dir) dirs + +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 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 + | [] -> + anomalylabstrm "" (str (locstr^": cannot find "^s^ + " in module"^(if List.length dirs > 1 then "s " else " ")) ++ + prlist_with_sep pr_coma pr_dirpath dirs) + | l -> + anomalylabstrm "" + (str (locstr^": found more than once object of name "^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 + +let arith_dir = ["Coq";"Arith"] +let arith_modules = [arith_dir] + +let narith_dir = ["Coq";"NArith"] + +let zarith_dir = ["Coq";"ZArith"] +let zarith_base_modules = [narith_dir;zarith_dir] + +let init_dir = ["Coq";"Init"] +let init_modules = [ + init_dir@["Datatypes"]; + init_dir@["Logic"]; + init_dir@["Specif"]; + init_dir@["Logic_Type"]; + init_dir@["Peano"]; + init_dir@["Wf"] +] + +let coq_id = id_of_string "Coq" +let init_id = id_of_string "Init" +let arith_id = id_of_string "Arith" +let datatypes_id = id_of_string "Datatypes" + +let logic_module = make_dir ["Coq";"Init";"Logic"] +let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"] +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 nat_path = make_path datatypes_module (id_of_string "nat") + +let glob_nat = IndRef (nat_path,0) + +let path_of_O = ((nat_path,0),1) +let path_of_S = ((nat_path,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") + +let glob_eq = IndRef (eq_path,0) +let glob_eqT = IndRef (eqT_path,0) + +type coq_sigma_data = { + proj1 : constr; + proj2 : constr; + elim : constr; + intro : constr; + typ : constr } + +type 'a delayed = unit -> 'a + +let build_sigma_set () = + { proj1 = init_constant ["Specif"] "projS1"; + proj2 = init_constant ["Specif"] "projS2"; + elim = init_constant ["Specif"] "sigS_rec"; + intro = init_constant ["Specif"] "existS"; + typ = init_constant ["Specif"] "sigS" } + +let build_sigma_type () = + { proj1 = init_constant ["Specif"] "projT1"; + proj2 = init_constant ["Specif"] "projT2"; + elim = init_constant ["Specif"] "sigT_rec"; + intro = init_constant ["Specif"] "existT"; + typ = init_constant ["Specif"] "sigT" } + +(* Equalities *) +type coq_leibniz_eq_data = { + eq : constr; + refl : constr; + ind : constr; + rrec : constr option; + rect : constr option; + congr: constr; + sym : constr } + +let lazy_init_constant dir id = lazy (init_constant dir id) + +(* Equality on Set *) +let coq_eq_eq = lazy_init_constant ["Logic"] "eq" +let coq_eq_refl = lazy_init_constant ["Logic"] "refl_equal" +let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind" +let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec" +let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect" +let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal" +let coq_eq_sym = lazy_init_constant ["Logic"] "sym_eq" +let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2" + +let build_coq_eq_data () = { + eq = Lazy.force coq_eq_eq; + refl = Lazy.force coq_eq_refl; + ind = Lazy.force coq_eq_ind; + 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 } + +let build_coq_eq () = Lazy.force coq_eq_eq +let build_coq_f_equal2 () = Lazy.force coq_f_equal2 + +(* Specif *) +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" + +(* The False proposition *) +let coq_False = lazy_init_constant ["Logic"] "False" + +(* The True proposition and its unique proof *) +let coq_True = lazy_init_constant ["Logic"] "True" +let coq_I = lazy_init_constant ["Logic"] "I" + +(* Connectives *) +let coq_not = lazy_init_constant ["Logic"] "not" +let coq_and = lazy_init_constant ["Logic"] "and" +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 + +let build_coq_False () = Lazy.force coq_False +let build_coq_not () = Lazy.force coq_not +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){x=y}+{~(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_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") diff --git a/interp/coqlib.mli b/interp/coqlib.mli new file mode 100644 index 00000000..7ac2a5c9 --- /dev/null +++ b/interp/coqlib.mli @@ -0,0 +1,126 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string list -> string -> global_reference +val gen_constant : string->string list -> string -> constr + +(* Search in several modules (not prefixed by "Coq") *) +val gen_constant_in_modules : string->string list list-> string -> constr +val arith_modules : string list list +val zarith_base_modules : string list list +val init_modules : string list list + +(*s Global references *) + +(* Modules *) +val logic_module : dir_path +val logic_type_module : dir_path + +(* Natural numbers *) +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 + +(* 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 + them at runtime. This is the purpose of the [constr delayed] and + [constr_pattern delayed] types. Objects of this time needs to be + applied to [()] to get the actual constr or pattern at runtime *) + +type 'a delayed = unit -> 'a + +(*s For Equality tactics *) +type coq_sigma_data = { + proj1 : constr; + proj2 : constr; + elim : constr; + intro : constr; + typ : constr } + +val build_sigma_set : coq_sigma_data delayed +val build_sigma_type : coq_sigma_data delayed + +type coq_leibniz_eq_data = { + eq : constr; + refl : constr; + ind : constr; + rrec : constr option; + rect : constr option; + congr: constr; + 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_eq : constr delayed (* = (build_coq_eq_data()).eq *) +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 + +(*s Connectives *) +(* The False proposition *) +val build_coq_False : constr delayed + +(* The True proposition and its unique proof *) +val build_coq_True : constr delayed +val build_coq_I : constr delayed + +(* Negation *) +val build_coq_not : constr delayed + +(* Conjunction *) +val build_coq_and : constr delayed + +(* Disjunction *) +val build_coq_or : constr delayed + +(* Existential quantifier *) +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_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 diff --git a/interp/doc.tex b/interp/doc.tex new file mode 100644 index 00000000..4d60ec34 --- /dev/null +++ b/interp/doc.tex @@ -0,0 +1,14 @@ + +\newpage +\section*{The interpretation of Coq front abstract syntax of terms} + +\ocwsection \label{library} +This chapter describes the translation from \Coq\ context-dependent +front abstract syntax of terms (\verb=front=} to and from the +context-free, untyped, raw form of constructions (\verb=rawconstr=). + +The modules translating back and forth the front abstract syntax are +organized as follows. + +\bigskip +\begin{center}\epsfig{file=library.dep.ps}\end{center} diff --git a/interp/genarg.ml b/interp/genarg.ml new file mode 100644 index 00000000..af3d805a --- /dev/null +++ b/interp/genarg.ml @@ -0,0 +1,228 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* pr_case_intro_pattern pll + | IntroWildcard -> str "_" + | IntroIdentifier id -> pr_id id + +and pr_case_intro_pattern = function + | [_::_ as pl] -> + str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" + | pll -> + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) + ++ str "]" + +type open_constr = Evd.evar_map * Term.constr +type open_constr_expr = constr_expr +type open_rawconstr = rawconstr_and_expr + +let rawwit_bool = BoolArgType +let globwit_bool = BoolArgType +let wit_bool = BoolArgType + +let rawwit_int = IntArgType +let globwit_int = IntArgType +let wit_int = IntArgType + +let rawwit_int_or_var = IntOrVarArgType +let globwit_int_or_var = IntOrVarArgType +let wit_int_or_var = IntOrVarArgType + +let rawwit_string = StringArgType +let globwit_string = StringArgType +let wit_string = StringArgType + +let rawwit_pre_ident = PreIdentArgType +let globwit_pre_ident = PreIdentArgType +let wit_pre_ident = PreIdentArgType + +let rawwit_intro_pattern = IntroPatternArgType +let globwit_intro_pattern = IntroPatternArgType +let wit_intro_pattern = IntroPatternArgType + +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_ref = RefArgType +let globwit_ref = RefArgType +let wit_ref = RefArgType + +let rawwit_quant_hyp = QuantHypArgType +let globwit_quant_hyp = QuantHypArgType +let wit_quant_hyp = QuantHypArgType + +let rawwit_sort = SortArgType +let globwit_sort = SortArgType +let wit_sort = SortArgType + +let rawwit_constr = ConstrArgType +let globwit_constr = ConstrArgType +let wit_constr = ConstrArgType + +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_casted_open_constr = CastedOpenConstrArgType +let globwit_casted_open_constr = CastedOpenConstrArgType +let wit_casted_open_constr = CastedOpenConstrArgType + +let rawwit_constr_with_bindings = ConstrWithBindingsArgType +let globwit_constr_with_bindings = ConstrWithBindingsArgType +let wit_constr_with_bindings = ConstrWithBindingsArgType + +let rawwit_bindings = BindingsArgType +let globwit_bindings = BindingsArgType +let wit_bindings = BindingsArgType + +let rawwit_red_expr = RedExprArgType +let globwit_red_expr = RedExprArgType +let wit_red_expr = RedExprArgType + +let wit_list0 t = List0ArgType t + +let wit_list1 t = List1ArgType t + +let wit_opt t = OptArgType t + +let wit_pair t1 t2 = PairArgType (t1,t2) + +let in_gen t o = (t,Obj.repr o) +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) -> + 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) -> + 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) -> + (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) -> + let (x1,x2) = Obj.magic l in + f (in_gen t1 x1) (in_gen t2 x2) + | _ -> failwith "Genarg: not a pair" + +let app_list0 f = function + | (List0ArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not a list0" + +let app_list1 f = function + | (List1ArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not a list1" + +let app_opt f = function + | (OptArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not an opt" + +let app_pair f1 f2 = function + | (PairArgType (t1,t2) as u, l) -> + let (o1,o2) = Obj.magic l in + let o1 = out_gen t1 (f1 (in_gen t1 o1)) in + let o2 = out_gen t2 (f2 (in_gen t2 o2)) in + (u, Obj.repr (o1,o2)) + | _ -> failwith "Genarg: not a pair" + +let unquote x = x + +type an_arg_of_this_type = Obj.t + +let in_generic t x = (t, Obj.repr x) diff --git a/interp/genarg.mli b/interp/genarg.mli new file mode 100644 index 00000000..59b6e10d --- /dev/null +++ b/interp/genarg.mli @@ -0,0 +1,262 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ('a list,'co,'ta) abstract_argument_type + +val wit_list1 : + ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type + +val wit_opt : + ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type + +val wit_pair : + ('a,'co,'ta) abstract_argument_type -> + ('b,'co,'ta) abstract_argument_type -> + ('a * 'b,'co,'ta) abstract_argument_type + +(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *) +type ('a,'b) generic_argument + +val fold_list0 : + (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c + +val fold_list1 : + (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c + +val fold_opt : + (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c + +val fold_pair : + (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) -> + ('a,'b) generic_argument -> 'c + +(* [app_list0] fails if applied to an argument not of tag [List0 t] + for some [t]; it's the responsability of the caller to ensure it *) + +val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> +('a,'b) generic_argument -> ('c,'d) generic_argument + +val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> +('a,'b) generic_argument -> ('c,'d) generic_argument + +val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> +('a,'b) generic_argument -> ('c,'d) generic_argument + +val app_pair : + (('a,'b) generic_argument -> ('c,'d) generic_argument) -> + (('a,'b) generic_argument -> ('c,'d) generic_argument) + -> ('a,'b) generic_argument -> ('c,'d) generic_argument + +(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le + polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel + de create *) +val create_arg : string -> + ('a,'co,'ta) abstract_argument_type + * ('globa,'globco,'globta) abstract_argument_type + * ('rawa,'rawco,'rawta) abstract_argument_type + +val exists_argtype : string -> bool + +type argument_type = + (* Basic types *) + | BoolArgType + | IntArgType + | IntOrVarArgType + | StringArgType + | PreIdentArgType + | IntroPatternArgType + | IdentArgType + | HypArgType + | RefArgType + (* Specific types *) + | SortArgType + | ConstrArgType + | ConstrMayEvalArgType + | QuantHypArgType + | TacticArgType + | CastedOpenConstrArgType + | ConstrWithBindingsArgType + | BindingsArgType + | RedExprArgType + | List0ArgType of argument_type + | List1ArgType of argument_type + | OptArgType of argument_type + | PairArgType of argument_type * argument_type + | ExtraArgType of string + +val genarg_tag : ('a,'b) generic_argument -> argument_type + +val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type + +(* We'd like + + [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument] + + with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a| + + in_generic is not typable; we replace the second argument by an absurd + type (with no introduction rule) +*) +type an_arg_of_this_type + +val in_generic : + argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument + +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 new file mode 100644 index 00000000..0929119c --- /dev/null +++ b/interp/modintern.ml @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + +(* +(* Since module components are not put in the nametab we try to locate +the module prefix *) +exception BadRef + +let lookup_qualid (modtype:bool) qid = + let rec make_mp mp = function + [] -> mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + in + let rec find_module_prefix dir n = + if n<0 then raise Not_found; + let dir',dir'' = list_chop n dir in + let id',dir''' = + match dir'' with + | hd::tl -> hd,tl + | _ -> anomaly "This list should not be empty!" + in + let qid' = make_qualid dir' id' in + try + match Nametab.locate qid' with + | ModRef mp -> mp,dir''' + | _ -> raise BadRef + with + Not_found -> find_module_prefix dir (pred n) + in + try Nametab.locate qid + with Not_found -> + let (dir,id) = repr_qualid qid in + let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in + let mp = + List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir' + in + if modtype then + ModTypeRef (make_ln mp (label_of_id id)) + else + ModRef (MPdot (mp,label_of_id id)) + +*) + +(* Search for the head of [qid] in [binders]. + If found, returns the module_path/kernel_name created from the dirpath + and the basename. Searches Nametab otherwise. +*) + +let lookup_module (loc,qid) = + try + Nametab.locate_module qid + with + | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) + +let lookup_modtype (loc,qid) = + try + Nametab.locate_modtype qid + with + | Not_found -> + 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) + +let rec interp_modtype env = function + | CMTEident qid -> + MTEident (lookup_modtype qid) + | CMTEwith (mty,decl) -> + let mty = interp_modtype env mty in + let decl = transl_with_decl env decl in + MTEwith(mty,decl) + + +let rec interp_modexpr env = function + | CMEident qid -> + MEident (lookup_module qid) + | CMEapply (me1,me2) -> + let me1 = interp_modexpr env me1 in + let me2 = interp_modexpr env me2 in + MEapply(me1,me2) + diff --git a/interp/modintern.mli b/interp/modintern.mli new file mode 100644 index 00000000..050d9f94 --- /dev/null +++ b/interp/modintern.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* module_type_ast -> module_type_entry + +val interp_modexpr : env -> module_ast -> module_expr + diff --git a/interp/ppextend.ml b/interp/ppextend.ml new file mode 100644 index 00000000..29fb7cc7 --- /dev/null +++ b/interp/ppextend.ml @@ -0,0 +1,58 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* h n + | PpHOVB n -> hov n + | PpHVB n -> hv n + | PpVB n -> v n + | PpTB -> t + +let ppcmd_of_cut = function + | PpTab -> tab () + | PpFnl -> fnl () + | PpBrk(n1,n2) -> brk(n1,n2) + | PpTbrk(n1,n2) -> tbrk(n1,n2) + +type unparsing = + | UnpMetaVar of int * parenRelation + | UnpListMetaVar of int * parenRelation * unparsing list + | UnpTerminal of string + | UnpBox of ppbox * unparsing list + | UnpCut of ppcut diff --git a/interp/ppextend.mli b/interp/ppextend.mli new file mode 100644 index 00000000..056b7a42 --- /dev/null +++ b/interp/ppextend.mli @@ -0,0 +1,48 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds -> std_ppcmds + +val ppcmd_of_cut : ppcut -> std_ppcmds + +type unparsing = + | UnpMetaVar of int * parenRelation + | UnpListMetaVar of int * parenRelation * unparsing list + | UnpTerminal of string + | UnpBox of ppbox * unparsing list + | UnpCut of ppcut diff --git a/interp/reserve.ml b/interp/reserve.ml new file mode 100644 index 00000000..72899676 --- /dev/null +++ b/interp/reserve.ml @@ -0,0 +1,95 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !reserve_table); + Summary.unfreeze_function = (fun r -> reserve_table := r); + Summary.init_function = (fun () -> reserve_table := Idmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let declare_reserved_type (loc,id) t = + if id <> root_of_id id then + user_err_loc(loc,"declare_reserved_type", + (pr_id id ++ str + " is not reservable: it must have no trailing digits, quote, or _")); + begin try + let _ = Idmap.find id !reserve_table in + user_err_loc(loc,"declare_reserved_type", + (pr_id id++str" is already bound to a type")) + with Not_found -> () end; + add_anonymous_leaf (in_reserved (id,t)) + +let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table + +open Rawterm + +let rec unloc = function + | RVar (_,id) -> RVar (dummy_loc,id) + | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args) + | 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 (dummy_loc, + (option_app unloc tyopt,ref (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) -> + RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2) + | RRec (_,fk,idl,bl,tyl,bv) -> + RRec (dummy_loc,fk,idl, + Array.map (List.map + (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty))) + bl, + Array.map unloc tyl, + Array.map unloc bv) + | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t) + | RSort (_,x) -> RSort (dummy_loc,x) + | RHole (_,x) -> RHole (dummy_loc,x) + | RRef (_,x) -> RRef (dummy_loc,x) + | REvar (_,x,l) -> REvar (dummy_loc,x,l) + | RPatVar (_,x) -> RPatVar (dummy_loc,x) + | RDynamic (_,x) -> RDynamic (dummy_loc,x) + +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) + else t + with Not_found -> t) + | Anonymous -> t diff --git a/interp/reserve.mli b/interp/reserve.mli new file mode 100644 index 00000000..a79e2c25 --- /dev/null +++ b/interp/reserve.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* rawconstr -> unit +val find_reserved_type : identifier -> rawconstr +val anonymize_if_reserved : name -> rawconstr -> rawconstr diff --git a/interp/symbols.ml b/interp/symbols.ml new file mode 100644 index 00000000..ed151d8e --- /dev/null +++ b/interp/symbols.ml @@ -0,0 +1,662 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* level * dir_path *) +let notation_level_map = ref Stringmap.empty + +(* Scopes table: scope_name -> symbol_interpretation *) +let scope_map = ref Stringmap.empty + +let empty_scope = { + notations = Stringmap.empty; + delimiters = None +} + +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 + +(**********************************************************************) +(* Operations on scopes *) + +let declare_scope scope = + try let _ = Stringmap.find scope !scope_map in () + with Not_found -> +(* Options.if_verbose message ("Creating scope "^scope);*) + scope_map := Stringmap.add scope empty_scope !scope_map + +let find_scope scope = + try Stringmap.find scope !scope_map + with Not_found -> error ("Scope "^scope^" is not declared") + +let check_scope sc = let _ = find_scope sc in () + +(**********************************************************************) +(* The global stack of scopes *) + +type scope_elem = Scope of scope_name | SingleNotation of string +type scopes = scope_elem list + +let scope_stack = ref [] + +let current_scopes () = !scope_stack + +(* TODO: push nat_scope, z_scope, ... in scopes summary *) + +(* Exportation of scopes *) +let cache_scope (_,(local,op,sc)) = + (match sc with Scope sc -> check_scope sc | _ -> ()); + scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack + +let subst_scope (_,subst,sc) = sc + +open Libobject + +let classify_scope (_,(local,_,_ as o)) = + if local then Dispose else Substitute o + +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); + subst_function = subst_scope; + classify_function = classify_scope; + export_function = export_scope } + +let open_close_scope (local,opening,sc) = + Lib.add_anonymous_leaf (inScope (local,opening,Scope sc)) + +let empty_scope_stack = [] + +let push_scope sc scopes = Scope sc :: scopes + +(**********************************************************************) +(* Delimiters *) + +let delimiters_map = ref Stringmap.empty + +let declare_delimiters scope key = + let sc = find_scope scope in + if sc.delimiters <> None && Options.is_verbose () then begin + let old = out_some sc.delimiters in + Options.if_verbose + 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 + Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc) + end; + delimiters_map := Stringmap.add key scope !delimiters_map + +let find_delimiters_scope loc key = + try Stringmap.find key !delimiters_map + with Not_found -> + user_err_loc + (loc, "find_delimiters", str ("Unknown scope delimiting key "^key)) + +(* Uninterpretation tables *) + +type interp_rule = + | NotationRule of scope_name option * notation + | SynDefRule of kernel_name + +(* We define keys for rawterm and aconstr to split the syntax entries + according to the key of the pattern (adapted from Chet Murthy by HH) *) + +type key = + | RefKey of global_reference + | Oth + +(* Scopes table : interpretation -> scope_name *) +let notations_key_table = ref Gmapl.empty +let numeral_key_table = Hashtbl.create 7 + +let rawconstr_key = function + | RApp (_,RRef (_,ref),_) -> RefKey ref + | RRef (_,ref) -> RefKey ref + | _ -> Oth + +let cases_pattern_key = function + | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref) + | _ -> Oth + +let aconstr_key = function + | AApp (ARef ref,args) -> RefKey ref, Some (List.length args) + | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args) + | ARef ref -> RefKey ref, Some 0 + | _ -> Oth, None + +let pattern_key = function + | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr) + | _ -> Oth + +(**********************************************************************) +(* Interpreting numbers (not in summary because functional objects) *) + +type num_interpreter = + (loc -> bigint -> rawconstr) + * (loc -> bigint -> name -> cases_pattern) option + +type num_uninterpreter = + rawconstr list * (rawconstr -> bigint option) + * (cases_pattern -> bigint option) option + +type required_module = global_reference * string list + +let numeral_interpreter_tab = + (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t) + +let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) = + 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)) + 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 () + with Not_found -> + user_err_loc (loc,"numeral_interpreter", + str ("Cannot interpret numbers 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 + | Some key -> Some (Some scope, Some key) + | None -> None + +let rec find_without_delimiters find (ntn_scope,ntn) = function + | Scope scope :: scopes -> + (* Is the expected ntn/numpr attached to the most recently open scope? *) + if Some scope = ntn_scope then + Some (None,None) + else + (* If the most recently open scope has a notation/numeral printer + but not the expected one then we need delimiters *) + if find scope then + find_with_delimiters ntn_scope + else + find_without_delimiters find (ntn_scope,ntn) scopes + | SingleNotation ntn' :: scopes -> + if ntn_scope = None & ntn = Some ntn' then + Some (None,None) + else + find_without_delimiters find (ntn_scope,ntn) scopes + | [] -> + (* Can we switch to [scope]? Yes if it has defined delimiters *) + find_with_delimiters ntn_scope + +(* Uninterpreted notation levels *) + +let declare_notation_level ntn level = + if not !Options.v7 & Stringmap.mem ntn !notation_level_map then + error ("Notation "^ntn^" is already assigned a level"); + notation_level_map := Stringmap.add ntn level !notation_level_map + +let level_of_notation ntn = + Stringmap.find ntn !notation_level_map + +(* The mapping between notations and their interpretation *) + +let declare_notation_interpretation ntn scopt pat df pp8only = + 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 + warning ("Notation "^ntn^" is 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; + 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) + | [] -> raise Not_found + +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 -> + user_err_loc + (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"")) + +let uninterp_notations c = + Gmapl.find (rawconstr_key c) !notations_key_table + +let uninterp_cases_pattern_notations c = + Gmapl.find (cases_pattern_key c) !notations_key_table + +let availability_of_notation (ntn_scope,ntn) scopes = + let f scope = + Stringmap.mem ntn (Stringmap.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 = + try + let (sc,numpr,_) = Hashtbl.find numeral_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 = + 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) + with Not_found -> raise No_match + +let availability_of_numeral printer_scope scopes = + let f scope = Hashtbl.mem numeral_interpreter_tab scope in + option_app snd (find_without_delimiters f (Some printer_scope,None) scopes) + +(* Miscellaneous *) + +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 -> [] + +(**********************************************************************) +(* Mapping classes to scopes *) + +open Classops + +let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t) + +let _ = Gmap.add CL_SORT "type_scope" Gmap.empty + +let declare_class_scope sc cl = + class_scope_map := Gmap.add cl sc !class_scope_map + +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 + | Var id -> CL_SECVAR id + | Const sp -> CL_CONST sp + | Ind ind_sp -> CL_IND ind_sp + | Prod (_,_,_) -> CL_FUN + | Sort _ -> CL_SORT + | _ -> raise Not_found + +let rec compute_arguments_scope t = + match kind_of_term (Reductionops.whd_betaiotazeta t) with + | Prod (_,t,u) -> + let sc = + try Some (find_class_scope (find_class t)) with Not_found -> None in + sc :: compute_arguments_scope u + | _ -> [] + +let declare_ref_arguments_scope ref = + let t = Global.type_of_global ref in + declare_arguments_scope ref (compute_arguments_scope t) + +(********************************) +(* Encoding notations as string *) + +type symbol = + | Terminal of string + | NonTerminal of identifier + | SProdList of identifier * symbol list + | Break of int + +let rec string_of_symbol = function + | NonTerminal _ -> ["_"] + | Terminal s -> [s] + | SProdList (_,l) -> + let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"] + | Break _ -> [] + +let make_notation_key symbols = + String.concat " " (List.flatten (List.map string_of_symbol symbols)) + +let decompose_notation_key s = + let len = String.length s in + let rec decomp_ntn dirs n = + if n>=len then dirs else + let pos = + try + String.index_from s n ' ' + with Not_found -> len + in + let tok = + match String.sub s n (pos-n) with + | "_" -> NonTerminal (id_of_string "_") + | s -> Terminal s in + decomp_ntn (tok::dirs) (pos+1) + in + decomp_ntn [] 0 + +(************) +(* Printing *) + +let pr_delimiters_info = function + | None -> str "No delimiting key" + | Some key -> str "Delimiting key is " ++ str key + +let classes_of_scope sc = + Gmap.fold (fun cl sc' l -> if sc = sc' then cl::l else l) !class_scope_map [] + +let pr_scope_classes sc = + let l = classes_of_scope sc in + if l = [] then mt() + else + 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) + +let pr_named_scope prraw scope sc = + (if scope = default_scope then + match Stringmap.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 -> + 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 + (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 -> + Some scope + | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope + | _::scopes -> find_default ntn scopes + | [] -> None + +let factorize_entries = function + | [] -> [] + | (ntn,c)::l -> + let (ntn,l_of_ntn,rest) = + List.fold_left + (fun (a',l,rest) (a,c) -> + if a = a' then (a',c::l,rest) else (a,[c],(a',l)::rest)) + (ntn,[c],[]) l in + (ntn,l_of_ntn)::rest + +let is_ident s = (* Poor analysis *) + String.length s <> 0 & is_letter s.[0] + +let browse_notation ntn map = + let find = + if String.contains ntn ' ' then (=) ntn + else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in + let l = + Stringmap.fold + (fun scope_name sc -> + Stringmap.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 + factorize_entries l + +let locate_notation prraw ntn = + let ntns = browse_notation ntn !scope_map in + if ntns = [] then + str "Unknown notation" + else + t (str "Notation " ++ + tab () ++ str "Scope " ++ tab () ++ fnl () ++ + prlist (fun (ntn,l) -> + let scope = find_default ntn !scope_stack in + prlist + (fun (sc,r,(_,df)) -> + hov 0 ( + pr_notation_info prraw df r ++ tbrk (1,2) ++ + (if sc = default_scope then mt () else (str ": " ++ str sc)) ++ + tbrk (1,2) ++ + (if Some sc = scope then str "(default interpretation)" else mt ()) + ++ fnl ())) + l) ntns) + +let collect_notation_in_scope scope sc known = + assert (scope <> default_scope); + Stringmap.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) + +let collect_notations stack = + fst (List.fold_left + (fun (all,knownntn as acc) -> function + | Scope scope -> + if List.mem_assoc scope all then acc + else + let (l,knownntn) = + collect_notation_in_scope scope (find_scope scope) knownntn in + ((scope,l)::all,knownntn) + | SingleNotation ntn -> + if List.mem ntn knownntn then (all,knownntn) + else + let ((_,r),(_,df),_) = + Stringmap.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 + | _ -> + (default_scope,[df,r])::all in + (all',ntn::knownntn)) + ([],[]) stack) + +let pr_visible_in_scope prraw (scope,ntns) = + let strm = + List.fold_right + (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm) + ntns (mt ()) in + (if scope = default_scope then + str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt()) + else + str "Visible in scope " ++ str scope) + ++ fnl () ++ strm + +let pr_scope_stack prraw stack = + List.fold_left + (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ()) + (mt ()) (collect_notations stack) + +let pr_visibility prraw = function + | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack) + | None -> pr_scope_stack prraw !scope_stack + +(**********************************************************************) +(* Mapping notations to concrete syntax *) + +type unparsing_rule = unparsing list * precedence + +(* Concrete syntax for symbolic-extension table *) +let printing_rules = + ref (Stringmap.empty : unparsing_rule Stringmap.t) + +let declare_notation_printing_rule ntn unpl = + printing_rules := Stringmap.add ntn unpl !printing_rules + +let find_notation_printing_rule ntn = + try Stringmap.find ntn !printing_rules + with Not_found -> anomaly ("No printing rule found for "^ntn) + +(**********************************************************************) +(* Synchronisation with reset *) + +let freeze () = + (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, + !delimiters_map, !notations_key_table, !printing_rules, + !class_scope_map) + +let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = + scope_map := scm; + notation_level_map := nlm; + scope_stack := scs; + delimiters_map := dlm; + arguments_scope := asc; + notations_key_table := fkm; + printing_rules := pprules; + class_scope_map := clsc + +let init () = + init_scope_map (); +(* + scope_stack := Stringmap.empty + arguments_scope := Refmap.empty +*) + notation_level_map := Stringmap.empty; + delimiters_map := Stringmap.empty; + notations_key_table := Gmapl.empty; + printing_rules := Stringmap.empty; + class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty + +let _ = + declare_summary "symbols" + { freeze_function = freeze; + unfreeze_function = unfreeze; + init_function = init; + survive_module = false; + survive_section = false } diff --git a/interp/symbols.mli b/interp/symbols.mli new file mode 100644 index 00000000..00d8e5ff --- /dev/null +++ b/interp/symbols.mli @@ -0,0 +1,160 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(* Open scope *) + +val current_scopes : unit -> scopes +val open_close_scope : + (* locality *) bool * (* open *) bool * scope_name -> unit + +(* Extend a list of scopes *) +val empty_scope_stack : scopes +val push_scope : scope_name -> scopes -> scopes + +(* Declare delimiters for printing *) + +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 *) + +(* 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 num_uninterpreter = + rawconstr list * (rawconstr -> bigint option) + * (cases_pattern -> bigint option) option + +type required_module = global_reference * string list +val declare_numeral_interpreter : scope_name -> required_module -> + num_interpreter -> num_uninterpreter -> unit + +(* Returns 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 + +(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *) +(* such numeral *) +val uninterp_numeral : rawconstr -> scope_name * bigint +val uninterp_cases_numeral : cases_pattern -> scope_name * bigint + +val availability_of_numeral : scope_name -> scopes -> delimiters option option + +(*s Declare and interpret back and forth a notation *) + +(* Binds a notation in a given scope to an interpretation *) +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 + +val declare_uninterpretation : interp_rule -> interpretation -> unit + +(* Returns the interpretation bound to a notation *) +val interp_notation : loc -> notation -> scope_name list -> + interpretation * ((dir_path * string) * scope_name option) + +(* Returns the possible notations for a given term *) +val uninterp_notations : rawconstr -> + (interp_rule * interpretation * int option) list +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 *) +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 *) + +(*s** Miscellaneous *) + +(* Checks for already existing notations *) +val exists_notation_in_scope : scope_name option -> notation -> + interpretation -> bool * bool + +(* Declares and looks for scopes associated to arguments of a global ref *) +val declare_arguments_scope: global_reference -> scope_name option list -> unit +val find_arguments_scope : global_reference -> scope_name option list + +val declare_class_scope : scope_name -> Classops.cl_typ -> unit +val declare_ref_arguments_scope : global_reference -> unit + +val compute_arguments_scope : Term.types -> scope_name option list + +(* Building notation key *) + +type symbol = + | Terminal of string + | NonTerminal of identifier + | SProdList of identifier * symbol list + | Break of int + +val make_notation_key : symbol list -> notation +val decompose_notation_key : notation -> symbol list + +(* Prints scopes (expect a pure aconstr printer *) +val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds +val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds +val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds + +val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds + +(**********************************************************************) +(*s Printing rules for notations *) + +(* Declare and look for the printing rule for symbolic notations *) +type unparsing_rule = unparsing list * precedence +val declare_notation_printing_rule : notation -> unparsing_rule -> unit +val find_notation_printing_rule : notation -> unparsing_rule + +(**********************************************************************) +(* Rem: printing rules for numerals are trivial *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml new file mode 100644 index 00000000..ef887d88 --- /dev/null +++ b/interp/syntax_def.ml @@ -0,0 +1,75 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !syntax_table); + Summary.unfreeze_function = (fun ft -> syntax_table := ft); + Summary.init_function = (fun () -> syntax_table := KNmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let add_syntax_constant kn c = + syntax_table := KNmap.add kn c !syntax_table + +let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) = + if Nametab.exists_cci sp then + errorlabstrm "cache_syntax_constant" + (pr_id (basename sp) ++ str " already exists"); + add_syntax_constant kn c; + Nametab.push_syntactic_definition (Nametab.Until i) sp kn; + if not onlyparse then + Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c) + +let open_syntax_constant i ((sp,kn),c) = + Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn + +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) + +let classify_syntax_constant (_,(local,_,_ as o)) = + if local then Dispose else Substitute o + +let export_syntax_constant (local,_,_ as o) = + if local then None else Some o + +let (in_syntax_constant, out_syntax_constant) = + declare_object {(default_object "SYNTAXCONSTANT") with + cache_function = cache_syntax_constant; + load_function = load_syntax_constant; + open_function = open_syntax_constant; + subst_function = subst_syntax_constant; + classify_function = classify_syntax_constant; + export_function = export_syntax_constant } + +let declare_syntactic_definition local id onlyparse c = + let _ = add_leaf id (in_syntax_constant (local,c,onlyparse)) in () + +let rec set_loc loc _ a = + rawconstr_of_aconstr_with_binders loc (fun id e -> (id,e)) (set_loc loc) () a + +let search_syntactic_definition loc kn = + set_loc loc () (KNmap.find kn !syntax_table) diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli new file mode 100644 index 00000000..0aec03c2 --- /dev/null +++ b/interp/syntax_def.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* identifier -> bool -> aconstr + -> unit + +val search_syntactic_definition : loc -> kernel_name -> rawconstr + + diff --git a/interp/topconstr.ml b/interp/topconstr.ml new file mode 100644 index 00000000..3ee3285b --- /dev/null +++ b/interp/topconstr.ml @@ -0,0 +1,702 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* let (id, e) = f id e in (Name id, e) + | Anonymous -> Anonymous, e + +let rec subst_rawvars l = function + | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r) + | r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *) + +let ldots_var = id_of_string ".." + +let rawconstr_of_aconstr_with_binders loc g f e = function + | AVar id -> RVar (loc,id) + | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args) + | AList (x,y,iter,tail,swap) -> + let t = f e tail in let it = f e iter in + let innerl = (ldots_var,t)::(if swap then [] else [x,RVar(loc,y)]) in + let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in + 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) + | AProd (na,ty,c) -> + let na,e = 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 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) + | ALetTuple (nal,(na,po),b,c) -> + RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c) + | AIf (c,(na,po),b1,b2) -> + 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) + | ASort x -> RSort (loc,x) + | AHole x -> RHole (loc,x) + | APatVar n -> RPatVar (loc,(false,n)) + | ARef x -> RRef (loc,x) + +let rec subst_pat subst pat = + match pat with + | PatVar _ -> pat + | PatCstr (loc,((kn,i),j),cpl,n) -> + let kn' = subst_kn subst kn + and cpl' = list_smartmap (subst_pat subst) cpl in + 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 + +let has_ldots = + List.exists + (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false) + +let compare_rawconstr f t1 t2 = match t1,t2 with + | RRef (_,r1), RRef (_,r2) -> r1 = r2 + | RVar (_,v1), RVar (_,v2) -> v1 = v2 + | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2 + | RLambda (_,na1,ty1,c1), RLambda (_,na2,ty2,c2) when na1 = na2 -> + f ty1 ty2 & f c1 c2 + | RProd (_,na1,ty1,c1), RProd (_,na2,ty2,c2) when na1 = na2 -> + f ty1 ty2 & f c1 c2 + | RHole _, RHole _ -> true + | RSort (_,s1), RSort (_,s2) -> s1 = s2 + | (RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _ + | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ + | _,(RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _ + | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) + -> error "Unsupported construction in recursive notations" + | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _ + -> false + +let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2 + +let discriminate_patterns 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 -> + if !diff = None then (diff := Some (v1,v2,(n>=nl)); true) + else + !diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n compare_rawconstr (aux (n+1)) c1 c2 in + 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 + +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 + | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args + | 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) -> + let f (_,idl,pat,rhs) = + bound_binders := idl@(!bound_binders); + (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; + option_iter + (fun (_,_,nl) -> List.iter (add_name bound_binders) 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) -> + ALetTuple (nal,(na,option_app aux po),aux b,aux c) + | RIf (loc,c,(na,po),b1,b2) -> + AIf (aux c,(na,option_app aux po),aux b1,aux b2) + | RCast (_,c,t) -> ACast (aux c,aux t) + | RSort (_,s) -> ASort s + | RHole (_,w) -> AHole w + | RRef (_,r) -> ARef r + | RPatVar (_,(_,n)) -> APatVar n + | RDynamic _ | RRec _ | REvar _ -> + error "Fixpoints, cofixpoints, existential variables and pattern-matching not \ +allowed in abbreviatable expressions" + + (* Recognizing recursive notations *) + and terminator_of_pat f1 ll1 lr1 = function + | RApp (loc,f2,l2) -> + if not (eq_rawconstr f1 f2) then error + "Cannot recognize the same head to both ends of the recursive pattern"; + let nl = List.length ll1 in + let nr = List.length lr1 in + if List.length l2 <> nl + nr + 1 then + 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 iter = + if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2) + else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in + (if order then y else x),(if order then x else y), aux iter, aux t, order + | _ -> error "One end of the recursive pattern is not an application" + + and make_aconstr_list f args = + let rec find_patterns acc = function + | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var -> + (* We've found the recursive part *) + let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in + AList (x,y,iter,term,lassoc) + | a::l -> find_patterns (a::acc) l + | [] -> error "Ill-formed recursive notation" + in find_patterns [] args + + in + let t = aux a in + (* Side effect *) + t, !found, !bound_binders + +let aconstr_of_rawconstr vars a = + let a,notbindingvars,binders = aconstr_and_vars_of_rawconstr a in + let check_type x = + if not (List.mem x notbindingvars or List.mem x binders) then + error ((string_of_id x)^" is unbound in the right-hand-side") in + List.iter check_type vars; + a + +let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) + +(* Pattern-matching rawconstr and aconstr *) + +let rec adjust_scopes = function + | _,[] -> [] + | [],a::args -> (None,a) :: adjust_scopes ([],args) + | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args) + +exception No_match + +let rec alpha_var id1 id2 = function + | (i1,i2)::_ when i1=id1 -> i2 = id2 + | (i1,i2)::_ when i2=id2 -> i1 = id1 + | _::idl -> alpha_var id1 id2 idl + | [] -> id1 = id2 + +let alpha_eq_val (x,y) = x = y + +let bind_env sigma var v = + try + let vvar = List.assoc var sigma in + if alpha_eq_val (v,vvar) then sigma + else raise No_match + with Not_found -> + (* TODO: handle the case of multiple occs in different scopes *) + (var,v)::sigma + +let rec match_ alp metas sigma a1 a2 = match (a1,a2) with + | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1 + | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma + | RRef (_,r1), ARef r2 when r1 = r2 -> sigma + | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma + | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 -> + List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2 + | RApp (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) + 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 + | RProd (_,na1,t1,b1), AProd (na2,t2,b2) -> + match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2 + | 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) + 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 + (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) -> + 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 + | (RDynamic _ | RRec _ | REvar _), _ + | _,_ -> raise No_match + +and match_alist alp metas sigma l1 l2 x iter termin lassoc = + (* match the iterator at least once *) + let sigma = List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in + (* Recover the recursive position *) + let rest = List.assoc ldots_var sigma in + (* Recover the first element *) + let t1 = List.assoc x sigma in + let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in + (* try to find the remaining elements or the terminator *) + let rec match_alist_tail alp metas sigma acc rest = + try + let sigma = match_ alp (ldots_var::metas) sigma rest iter in + let rest = List.assoc ldots_var sigma in + let t = List.assoc x sigma in + let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in + match_alist_tail alp metas sigma (t::acc) rest + with No_match -> + List.rev acc, match_ alp metas sigma rest termin in + 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 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_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = + if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then + match_ alp metas sigma rhs1 rhs2 + else raise No_match + +type scope_name = string + +type interpretation = + (identifier * (scope_name option * scope_name list)) list * aconstr + +let match_aconstr c (metas_scl,pat) = + let subst = match_ [] (List.map fst metas_scl) [] c pat in + (* Reorder canonically the substitution *) + let find x subst = + try List.assoc x subst + with Not_found -> + (* Happens for binders bound to Anonymous *) + (* Find a better way to propagate Anonymous... *) + RVar (dummy_loc,x) in + List.map (fun (x,scl) -> (find x subst,scl)) metas_scl + +(**********************************************************************) +(*s Concrete syntax for terms *) + +type notation = string + +type explicitation = ExplByPos of int | ExplByName of identifier + +type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) + +type cases_pattern_expr = + | CPatAlias of loc * cases_pattern_expr * identifier + | CPatCstr of loc * reference * cases_pattern_expr list + | CPatAtom of loc * reference option + | CPatNotation of loc * notation * cases_pattern_expr list + | CPatNumeral of loc * Bignat.bigint + | CPatDelimiters of loc * string * cases_pattern_expr + +type constr_expr = + | CRef of reference + | CFix of loc * identifier located * fixpoint_expr list + | CCoFix of loc * identifier located * cofixpoint_expr list + | CArrow of loc * constr_expr * constr_expr + | CProdN of loc * (name located list * constr_expr) list * constr_expr + | CLambdaN of loc * (name located list * constr_expr) list * constr_expr + | CLetIn of loc * name located * constr_expr * 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) * + (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) + * constr_expr * constr_expr + | CHole of loc + | CPatVar of loc * (bool * patvar) + | CEvar of loc * existential_key + | CSort of loc * rawsort + | CCast of loc * constr_expr * constr_expr + | CNotation of loc * notation * constr_expr list + | CNumeral of loc * Bignat.bigint + | CDelimiters of loc * string * constr_expr + | CDynamic of loc * Dyn.t + +and fixpoint_expr = + identifier * int * local_binder list * constr_expr * constr_expr + +and local_binder = + | LocalRawDef of name located * constr_expr + | LocalRawAssum of name located list * constr_expr + +and cofixpoint_expr = + identifier * local_binder list * constr_expr * constr_expr + +(***********************) +(* For binders parsing *) + +let rec local_binders_length = function + | [] -> 0 + | LocalRawDef _::bl -> 1 + local_binders_length bl + | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl + +let names_of_local_assums bl = + List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl) + +(**********************************************************************) +(* Functions on constr_expr *) + +let constr_loc = function + | CRef (Ident (loc,_)) -> loc + | CRef (Qualid (loc,_)) -> loc + | CFix (loc,_,_) -> loc + | CCoFix (loc,_,_) -> loc + | CArrow (loc,_,_) -> loc + | CProdN (loc,_,_) -> loc + | CLambdaN (loc,_,_) -> loc + | CLetIn (loc,_,_,_) -> loc + | 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 + | CNotation (loc,_,_) -> loc + | CNumeral (loc,_) -> loc + | CDelimiters (loc,_,_) -> loc + | CDynamic _ -> dummy_loc + +let cases_pattern_loc = function + | CPatAlias (loc,_,_) -> loc + | CPatCstr (loc,_,_) -> loc + | CPatAtom (loc,_) -> loc + | CPatNotation (loc,_,_) -> loc + | CPatNumeral (loc,_) -> loc + | CPatDelimiters (loc,_,_) -> loc + +let occur_var_constr_ref id = function + | Ident (loc,id') -> id = id' + | Qualid _ -> false + +let rec occur_var_constr_expr id = function + | CRef r -> occur_var_constr_ref id r + | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b + | CAppExpl (loc,(_,r),l) -> + occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l + | CApp (loc,(_,f),l) -> + occur_var_constr_expr id f or + List.exists (fun (a,_) -> occur_var_constr_expr id a) l + | 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 + | 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 + | CCases (loc,_,_,_) + | COrderedCase (loc,_,_,_,_) + | CLetTuple (loc,_,_,_,_) + | CIf (loc,_,_,_,_) + | CFix (loc,_,_) + | CCoFix (loc,_,_) -> + Pp.warning "Capture check in multiple binders not done"; false + +and occur_var_binders id b = function + | (idl,a)::l -> + occur_var_constr_expr id a or + (not (List.mem (Name id) (snd (List.split idl))) + & occur_var_binders id b l) + | [] -> occur_var_constr_expr id b + +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 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) + +(* 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 map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e + +let map_binders f g e bl = + (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in + let (e,rbl) = List.fold_left h (e,[]) bl in + (e, List.rev rbl) + +let map_local_binders f g e bl = + (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let h (e,bl) = function + LocalRawAssum(nal,ty) -> + (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl) + | LocalRawDef((loc,na),ty) -> + (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in + let (e,rbl) = List.fold_left h (e,[]) bl in + (e, List.rev rbl) + +let map_constr_expr_with_binders f g e = function + | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b) + | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l) + | CApp (loc,(p,a),l) -> + CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l) + | CProdN (loc,bl,b) -> + let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b) + | 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) + | 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) -> + (* 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' = + List.fold_right + (fun (tm,(na,indnal)) e -> + option_fold_right + (fun t -> + let ids = names_of_cases_indtype t in + List.fold_right g ids) + indnal (option_fold_right (name_fold g) na e)) + a e + in + CCases (loc,(option_app (f e) po, 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 + CLetTuple (loc,nal,(ona,option_app (f e'') po),f e b,f e' c) + | CIf (loc,c,(ona,po),b1,b2) -> + let e' = option_fold_right (name_fold g) ona e in + CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2) + | CFix (loc,id,dl) -> + CFix (loc,id,List.map (fun (id,n,bl,t,d) -> + let (e',bl') = map_local_binders f g e bl in + let t' = f e' t in + (* Note: fix names should be inserted before the arguments... *) + let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in + let d' = f e'' d in + (id,n,bl',t',d')) dl) + | CCoFix (loc,id,dl) -> + CCoFix (loc,id,List.map (fun (id,bl,t,d) -> + let (e',bl') = map_local_binders f g e bl in + let t' = f e' t in + let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in + let d' = f e'' d in + (id,bl',t',d')) dl) + +(* Used in constrintern *) +let rec replace_vars_constr_expr l = function + | CRef (Ident (loc,id)) as x -> + (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x) + | c -> map_constr_expr_with_binders replace_vars_constr_expr + (fun id l -> List.remove_assoc id l) l c + +(**********************************************************************) +(* 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 + +type module_type_ast = + | CMTEident of qualid located + | CMTEwith of module_type_ast * with_declaration_ast + +type module_ast = + | CMEident of qualid located + | CMEapply of module_ast * module_ast diff --git a/interp/topconstr.mli b/interp/topconstr.mli new file mode 100644 index 00000000..f4a82a3a --- /dev/null +++ b/interp/topconstr.mli @@ -0,0 +1,172 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (identifier -> 'a -> identifier * 'a) -> + ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr + +val subst_aconstr : Names.substitution -> aconstr -> aconstr + +val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr + +(* [match_aconstr metas] match a rawconstr against an aconstr with + metavariables in [metas]; it raises [No_match] if the matching fails *) +exception No_match + +type scope_name = string +type interpretation = + (identifier * (scope_name option * scope_name list)) list * aconstr + +val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation -> + (rawconstr * (scope_name option * scope_name list)) list + +(*s Concrete syntax for terms *) + +type notation = string + +type explicitation = ExplByPos of int | ExplByName of identifier + +type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) + +type cases_pattern_expr = + | CPatAlias of loc * cases_pattern_expr * identifier + | CPatCstr of loc * reference * cases_pattern_expr list + | CPatAtom of loc * reference option + | CPatNotation of loc * notation * cases_pattern_expr list + | CPatNumeral of loc * Bignat.bigint + | CPatDelimiters of loc * string * cases_pattern_expr + +type constr_expr = + | CRef of reference + | CFix of loc * identifier located * fixpoint_expr list + | CCoFix of loc * identifier located * cofixpoint_expr list + | CArrow of loc * constr_expr * constr_expr + | CProdN of loc * (name located list * constr_expr) list * constr_expr + | CLambdaN of loc * (name located list * constr_expr) list * constr_expr + | CLetIn of loc * name located * constr_expr * 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) * + (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) + * constr_expr * constr_expr + | CHole of loc + | CPatVar of loc * (bool * patvar) + | CEvar of loc * existential_key + | CSort of loc * rawsort + | CCast of loc * constr_expr * constr_expr + | CNotation of loc * notation * constr_expr list + | CNumeral of loc * Bignat.bigint + | CDelimiters of loc * string * constr_expr + | CDynamic of loc * Dyn.t + +and fixpoint_expr = + identifier * int * local_binder list * constr_expr * constr_expr + +and cofixpoint_expr = + identifier * local_binder list * constr_expr * constr_expr + +and local_binder = + | LocalRawDef of name located * constr_expr + | LocalRawAssum of name located list * constr_expr + + +val constr_loc : constr_expr -> loc + +val cases_pattern_loc : cases_pattern_expr -> loc + +val replace_vars_constr_expr : + (identifier * identifier) list -> constr_expr -> constr_expr + +val occur_var_constr_expr : identifier -> constr_expr -> bool + +(* Specific function for interning "in indtype" syntax of "match" *) +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 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 + +(* For binders parsing *) + +(* Includes let binders *) +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 + +(* 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)] *) + +val map_constr_expr_with_binders : + ('a -> constr_expr -> constr_expr) -> + (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr + +(* 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 + +type module_type_ast = + | CMTEident of qualid located + | CMTEwith of module_type_ast * with_declaration_ast + +type module_ast = + | CMEident of qualid located + | CMEapply of module_ast * module_ast + +(* Special identifier to encode recursive notations *) +val ldots_var : identifier -- cgit v1.2.3