diff options
Diffstat (limited to 'plugins')
44 files changed, 336 insertions, 299 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4c6156a38..4a691e442 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -130,8 +130,8 @@ type cinfo= ci_nhyps: int} (* # projectable args *) let family_eq f1 f2 = match f1, f2 with - | Prop Pos, Prop Pos - | Prop Null, Prop Null + | Set, Set + | Prop, Prop | Type _, Type _ -> true | _ -> false diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 1e0589fac..4ede11b5c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -596,19 +596,18 @@ let warns () = let rec locate_ref = function | [] -> [],[] - | r::l -> - let q = qualid_of_reference r in - let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None + | qid::l -> + let mpo = try Some (Nametab.locate_module qid) with Not_found -> None and ro = - try Some (Smartlocate.global_with_alias r) + try Some (Smartlocate.global_with_alias qid) with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with - | None, None -> Nametab.error_global_not_found q + | None, None -> Nametab.error_global_not_found qid | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_ambiguous_name (q.CAst.v,mp,r); + warning_ambiguous_name (qid,mp,r); let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 77f1fb5ef..54fde2ca4 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -13,14 +13,14 @@ open Names open Libnames -val simple_extraction : reference -> unit -val full_extraction : string option -> reference list -> unit -val separate_extraction : reference list -> unit +val simple_extraction : qualid -> unit +val full_extraction : string option -> qualid list -> unit +val separate_extraction : qualid list -> unit val extraction_library : bool -> Id.t -> unit (* For the test-suite : extraction to a temporary file + ocamlc on it *) -val extract_and_compile : reference list -> unit +val extract_and_compile : qualid list -> unit (* For debug / external output via coqtop.byte + Drop : *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5aee70194..71e09992c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -488,7 +488,7 @@ and extract_really_ind env kn mib = Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if List.is_empty l then raise (I Standard); - if Option.is_empty mib.mind_record then raise (I Standard); + if mib.mind_record == Declarations.NotRecord then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match Constr.kind t with @@ -1065,11 +1065,14 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_typ (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_typ (EConstr.of_constr pb.proj_body)) + let ind = pb.Declarations.proj_ind in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1078,11 +1081,14 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_def (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_def (EConstr.of_constr pb.proj_body)) + let ind = pb.Declarations.proj_ind in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 5bf944434..a8baeaf1b 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -194,17 +194,17 @@ val find_custom_match : ml_branch array -> string (*s Extraction commands. *) val extraction_language : lang -> unit -val extraction_inline : bool -> reference list -> unit +val extraction_inline : bool -> qualid list -> unit val print_extraction_inline : unit -> Pp.t val reset_extraction_inline : unit -> unit val extract_constant_inline : - bool -> reference -> string list -> string -> unit + bool -> qualid -> string list -> string -> unit val extract_inductive : - reference -> string -> string list -> string option -> unit + qualid -> string -> string list -> string option -> unit type int_or_id = ArgInt of int | ArgId of Id.t -val extraction_implicit : reference -> int_or_id list -> unit +val extraction_implicit : qualid -> int_or_id list -> unit (*s Table of blacklisted filenames *) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 30deb6f49..7e54bc8ad 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -17,7 +17,6 @@ open Goptions open Tacmach.New open Tacticals.New open Tacinterp -open Libnames open Stdarg open Tacarg open Pcoq.Prim @@ -127,7 +126,7 @@ let normalize_evaluables= open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference +let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a158fc8ff..31496513a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -627,7 +627,7 @@ let build_scheme fas = Smartlocate.global_with_alias f with Not_found -> user_err ~hdr:"FunInd.build_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) + (str "Cannot find " ++ Libnames.pr_qualid f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in @@ -668,7 +668,7 @@ let build_case_scheme fa = try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) in + (str "Cannot find " ++ Libnames.pr_qualid f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Constant.repr3 first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 33aeafef8..97f9acdb3 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -36,5 +36,5 @@ exception No_graph_found val make_scheme : Evd.evar_map ref -> (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list -val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit +val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 9899b7b21..a2d31780d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -168,7 +168,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ - Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ + Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg @@ -181,11 +181,11 @@ let warning_error names e = let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in warn_cannot_define_graph (names,error) | Defining_principle e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then CErrors.print e else mt () in warn_cannot_define_principle (names,error) | _ -> raise e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index cd640eebd..489a40ed0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -362,17 +362,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in + let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in let ind_kn = fst (locate_with_msg - (pr_reference f_R_mut++str ": Not an inductive type!") + (pr_qualid f_R_mut++str ": Not an inductive type!") locate_ind f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = CAst.map (fun n -> Ident n) fname in - locate_with_msg - (pr_reference f_ref++str ": Not an inductive type!") + let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in + locate_with_msg + (pr_qualid f_ref++str ": Not an inductive type!") locate_constant f_ref in @@ -477,7 +477,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,CAst.make @@ Ident fname,None) , + (None,qualid_of_ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -487,7 +487,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -544,9 +544,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) - in + Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")) + in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in @@ -727,12 +727,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof () let rec add_args id new_args = CAst.map (function - | CRef (r,_) as b -> - begin match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((None,r,None),new_args) - | _ -> b - end + | CRef (qid,_) as b -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((None,qid,None),new_args) + else b | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) @@ -746,13 +744,10 @@ let rec add_args id new_args = CAst.map (function add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) - | CAppExpl((pf,r,us),exprl) -> - begin - match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) - end + | CAppExpl((pf,qid,us),exprl) -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl)) + else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl) | CApp((pf,b),bl) -> CApp((pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) @@ -888,7 +883,7 @@ let make_graph (f_ref : GlobRef.t) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) nal | Constrexpr.CLocalPattern _ -> assert false ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index c6faa142a..4eee2c7a4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -31,9 +31,7 @@ let id_of_name = function Name id -> id | _ -> raise Not_found -let locate ref = - let {CAst.v=qid} = qualid_of_reference ref in - Nametab.locate qid +let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 346b21ef2..7e52ee224 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array val id_of_name : Name.t -> Id.t -val locate_ind : Libnames.reference -> inductive -val locate_constant : Libnames.reference -> Constant.t +val locate_ind : Libnames.qualid -> inductive +val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : - Pp.t -> (Libnames.reference -> 'a) -> - Libnames.reference -> 'a + Pp.t -> (Libnames.qualid -> 'a) -> + Libnames.qualid -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list val list_union_eq : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index aa49148fc..7298342e1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = CAst.make @@ Libnames.Ident na in + let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1577,7 +1577,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in + let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f2899ab63..660e29ca8 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -793,17 +793,12 @@ END (* ********************************************************************* *) -let eq_constr x y = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let evd = Tacmach.New.project gl in - match EConstr.eq_constr_universes env evd x y with - | Some _ -> Proofview.tclUNIT () - | None -> Tacticals.New.tclFAIL 0 (str "Not equal") - end - TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] +| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] +END + +TACTIC EXTEND constr_eq_strict +| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] END TACTIC EXTEND constr_eq_nounivs diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 642e52155..35ed14fc1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -173,7 +173,7 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] END -let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global let glob_hints_path_atom ist = Hints.glob_hints_path_atom @@ -189,7 +189,7 @@ ARGUMENT EXTEND hints_path_atom END let pr_hints_path prc prx pry c = Hints.pp_hints_path c -let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c let glob_hints_path ist = Hints.glob_hints_path ARGUMENT EXTEND hints_path diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index d7d642e50..620f14707 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -39,11 +39,12 @@ let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac -let reference_to_id = CAst.map_with_loc (fun ?loc -> function - | Libnames.Ident id -> id - | Libnames.Qualid _ -> - CErrors.user_err ?loc - (str "This expression should be a simple identifier.")) +let reference_to_id qid = + if Libnames.qualid_is_ident qid then + CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -199,8 +200,7 @@ GEXTEND Gram verbose most of the time. *) fresh_id: [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - Locus.ArgVar (CAst.make ~loc:!@loc id) ] ] + | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -475,7 +475,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ] + [ Feedback.msg_notice (Tacintern.print_ltac r) ] END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY @@ -483,7 +483,7 @@ VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY [ Tacentries.print_located_tactic r ] END -let pr_ltac_ref = Libnames.pr_reference +let pr_ltac_ref = Libnames.pr_qualid let pr_tacdef_body tacdef_body = let id, redef, body = @@ -510,8 +510,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition ({CAst.v=Ident r},_) -> r - | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater + | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; st diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 352e92c2a..1f56244c7 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe FilliĆ¢tre *) -open Libnames open Constrexpr open Constrexpr_ops open Stdarg @@ -49,7 +48,7 @@ module Tactic = Pltac open Pcoq -let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type @@ -68,7 +67,7 @@ GEXTEND Gram Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in [CLocalAssum ([id], default_binder_kind, typ)] ] ]; diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 2189e224f..f1634f156 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -67,13 +67,13 @@ let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in Rewrite.pr_strategy prc prr s let pr_glob_strategy prc prlc _ (s : glob_strategy) = let prr = Pptactic.pr_red_expr (Ppconstr.pr_constr_expr, Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_reference, + Pputils.pr_or_by_notation Libnames.pr_qualid, Ppconstr.pr_constr_expr) in Rewrite.pr_strategy prc prr s diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 05005c733..31bc34a32 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -156,7 +156,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> - TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 4c075d413..c5aa542fd 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -21,8 +21,8 @@ val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry -val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry -val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry +val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry +val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e19a95e84..09179dad3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -17,7 +17,6 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Libnames open Notation_gram open Tactypes open Locus @@ -1109,8 +1108,8 @@ let pr_goal_selector ~toplevel s = pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; pr_lpattern = pr_lconstr_pattern_expr; - pr_constant = pr_or_by_notation pr_reference; - pr_reference = pr_reference; + pr_constant = pr_or_by_notation pr_qualid; + pr_reference = pr_qualid; pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; @@ -1323,7 +1322,7 @@ let () = let open Genprint in register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) pr_global; + pr_qualid (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 @@ -1357,7 +1356,7 @@ let () = ; Genprint.register_print0 wit_red_expr - (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr))) (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index cd04f4ae9..01c52c413 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1773,11 +1773,11 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = (((CAst.make @@ Name n),None), Explicit, - CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args)) + CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] @@ -1791,17 +1791,17 @@ let anew_instance global binders instance fields = let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)] + [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)] + [(qualid_of_ident (Id.of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)] + [(qualid_of_ident (Id.of_string "transitivity"),lemma)] let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1825,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1842,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1949,16 +1949,15 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let make_tactic name = let open Tacexpr in - let tacpath = Libnames.qualid_of_string name in - let tacname = CAst.make @@ Qualid tacpath in - TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, [])))) + let tacqid = Libnames.qualid_of_string name in + TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> @@ -2008,7 +2007,7 @@ let add_morphism glob binders m s n = let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( - (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index cc9c2046d..84baea964 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,11 +199,12 @@ let id_of_name = function let basename = Nametab.basename_of_global ref in basename | Sort s -> - begin + begin match ESorts.kind sigma s with - | Sorts.Prop _ -> Label.to_id (Label.make "Prop") - | Sorts.Type _ -> Label.to_id (Label.make "Type") - end + | Sorts.Prop -> Label.to_id (Label.make "Prop") + | Sorts.Set -> Label.to_id (Label.make "Set") + | Sorts.Type _ -> Label.to_id (Label.make "Type") + end | _ -> fail() diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index fada7424c..98d451536 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -449,12 +449,12 @@ let register_ltac local tacl = in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body - | Tacexpr.TacticRedefinition (ident, body) -> + | Tacexpr.TacticRedefinition (qid, body) -> let kn = - try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v + try Tacenv.locate_tactic qid with Not_found -> - CErrors.user_err ?loc:ident.CAst.loc - (str "There is no Ltac named " ++ pr_reference ident ++ str ".") + CErrors.user_err ?loc:qid.CAst.loc + (str "There is no Ltac named " ++ pr_qualid qid ++ str ".") in UpdateTac kn, body in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 3f804ee8d..2bfbbe2e1 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -65,7 +65,7 @@ val create_ltac_quotation : string -> val print_ltacs : unit -> unit (** Display the list of ltac definitions currently available. *) -val print_located_tactic : Libnames.reference -> unit +val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) type _ ty_sig = diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index d51de8c65..06d2711ad 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 01eead164..71e1edfd7 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index cef5bb1b8..481fc30df 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -92,88 +92,83 @@ let intern_or_var f ist = function let intern_int_or_var = intern_or_var (fun (n : int) -> n) let intern_string_or_var = intern_or_var (fun (s : string) -> s) -let intern_global_reference ist = function - | {CAst.loc;v=Ident id} when find_var id ist -> - ArgVar (make ?loc id) - | r -> - let {CAst.loc} as lqid = qualid_of_reference r in - try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> error_global_not_found lqid - -let intern_ltac_variable ist = function - | {loc;v=Ident id} -> - if find_var id ist then - (* A local variable of any type *) - ArgVar (make ?loc id) - else raise Not_found - | _ -> - raise Not_found - -let intern_constr_reference strict ist = function - | {v=Ident id} as r when not strict && find_hyp id ist -> - (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) - | {v=Ident id} as r when find_var id ist -> - (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None)) - | r -> - let {loc} as lqid = qualid_of_reference r in - DAst.make @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (make @@ CRef (r,None)) +let intern_global_reference ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else + try ArgArg (qid.CAst.loc,locate_global_with_alias qid) + with Not_found -> error_global_not_found qid + +let intern_ltac_variable ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (* A local variable of any type *) + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else raise Not_found + +let intern_constr_reference strict ist qid = + let id = qualid_basename qid in + if qualid_is_ident qid && not strict && find_hyp (qualid_basename qid) ist then + (DAst.make @@ GVar id), Some (make @@ CRef (qid,None)) + else if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (qid,None)) + else + DAst.make @@ GRef (locate_global_with_alias qid,None), + if strict then None else Some (make @@ CRef (qid,None)) (* Internalize an isolated reference in position of tactic *) -let intern_isolated_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in +let intern_isolated_global_tactic_reference qid = + let loc = qid.CAst.loc in TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) -let intern_isolated_tactic_reference strict ist r = +let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A global tactic *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Internalize an applied tactic reference *) -let intern_applied_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in - ArgArg (loc,Tacenv.locate_tactic qid) +let intern_applied_global_tactic_reference qid = + ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid) -let intern_applied_tactic_reference ist r = +let intern_applied_tactic_reference ist qid = (* An ltac reference *) - try intern_ltac_variable ist r + try intern_ltac_variable ist qid with Not_found -> (* A global tactic *) - try intern_applied_global_tactic_reference r + try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) -let intern_non_tactic_reference strict ist r = +let intern_non_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A constr reference *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Tolerance for compatibility, allow not to use "ltac:" *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) - match r with - | {loc;v=Ident id} when not strict -> - let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in + if qualid_is_ident qid && not strict then + let id = qualid_basename qid in + let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat - | _ -> - (* Reference not found *) - error_global_not_found (qualid_of_reference r) + else + (* Reference not found *) + error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -269,7 +264,7 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) - let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in + let c, p = intern_constr ist (make @@ CRef (qualid_of_ident id, None)) in match DAst.get c with | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) @@ -277,16 +272,15 @@ let intern_destruction_arg ist = function clear,ElimOnIdent (make ?loc id) let short_name = function - | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id) + | {v=AN qid} when qualid_is_ident qid && not !strict_check -> + Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) | _ -> None -let intern_evaluable_global_reference ist r = - let lqid = qualid_of_reference r in - try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid) +let intern_evaluable_global_reference ist qid = + try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> - match r with - | {loc;v=Ident id} when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found lqid + if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) + else error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -296,14 +290,19 @@ let intern_evaluable_reference_or_by_notation ist = function (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) -let intern_evaluable ist = function - | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id) - | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some (make ?loc id)) - | r -> - let e = intern_evaluable_reference_or_by_notation ist r in - let na = short_name r in - ArgArg (e,na) +let intern_evaluable ist r = + let f ist r = + let e = intern_evaluable_reference_or_by_notation ist r in + let na = short_name r in + ArgArg (e,na) + in + match r with + | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist -> + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist -> + let id = qualid_basename qid in + ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id)) + | _ -> f ist r let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) @@ -356,7 +355,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 04dd7d6e9..9d1cc1643 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -361,7 +361,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -377,14 +377,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id) + | _ -> error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -643,7 +643,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (make ?loc @@ qualid_of_ident id)) + error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -925,7 +925,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (make ?loc id) else - let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in + let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 5e4c9214a..e9ce306e8 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -42,11 +42,11 @@ let pr_ring_mod = function | Ring_kind Abstract -> str "abstract" | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 84b29a0bf..e4d17f250 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -148,8 +148,7 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let env = Global.env () in - let vars = Univops.universes_of_constr env c in + let vars = Univops.universes_of_constr c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.ml +++ b/plugins/setoid_ring/newring_ast.ml @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 5571c5420..6ba937a2f 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -88,7 +88,7 @@ type ssripat = | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of ssrview (* /view *) + | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 2a31157be..54f3f9c71 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -858,7 +858,7 @@ open Util (** Constructors for constr_expr *) let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) -let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index f929e9430..23cbf49c0 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -417,8 +417,6 @@ let rwcltac cl rdx dir sr gl = then errorstrm Pp.(str "Rewriting impacts evars") else errorstrm Pp.(str "Dependent type error in rewrite of " ++ pr_constr_env (pf_env gl) (project gl) (Term.mkNamedLambda pattern_id (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) - | CErrors.UserError _ as e -> raise e - | e -> anomaly ("cvtac's exception: " ^ Printexc.to_string e); in tclTHEN cvtac' rwtac gl diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 2c046190f..7fe2421f9 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = let cl = EConstr.Unsafe.to_constr cl in try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++ @@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in - let gl = pf_merge_uc ucst gl in Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl open Util diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 8207bc11e..46fde4115 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -119,13 +119,10 @@ let intro_end = Ssrcommon.tcl0G (isCLR_CONSUME) (** [=> _] *****************************************************************) -let intro_clear ids future_ipats = +let intro_clear ids = Goal.enter begin fun gl -> let _, clear_ids, ren = List.fold_left (fun (used_ids, clear_ids, ren) id -> - if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin - used_ids, id :: clear_ids, ren - end else let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in (new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren)) (Tacmach.New.pf_ids_of_hyps gl, [], []) ids @@ -213,22 +210,22 @@ let tclLOG p t = tclUNIT () end -let rec ipat_tac1 future_ipats ipat : unit tactic = +let rec ipat_tac1 ipat : unit tactic = match ipat with - | IPatView l -> - Ssrview.tclIPAT_VIEWS ~views:l - ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats) + | IPatView (clear_if_id,l) -> + Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id + ~conclusion:(fun ~to_clear:clr -> intro_clear clr) | IPatDispatch ipatss -> - tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) [] + tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) [] | IPatId id -> Ssrcommon.tclINTRO_ID id | IPatCase ipatss -> - tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss + tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss | IPatInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) - future_ipats ipatss + ipatss | IPatAnon Drop -> intro_drop | IPatAnon One -> Ssrcommon.tclINTRO_ANON @@ -239,7 +236,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatClear ids -> tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats + intro_clear (List.map Ssrcommon.hyp_id ids) | IPatSimpl (Simpl n) -> V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) @@ -256,17 +253,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatTac t -> t -and ipat_tac future_ipats pl : unit tactic = +and ipat_tac pl : unit tactic = match pl with | [] -> tclUNIT () | pat :: pl -> - Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*> + Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*> isTICK pat <*> - ipat_tac future_ipats pl + ipat_tac pl -and tclIORPAT tac future_ipats = function +and tclIORPAT tac = function | [[]] -> tac - | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p) + | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) let split_at_first_case ipats = let rec loop acc = function @@ -282,12 +279,27 @@ let ssr_exception is_on = function let option_to_list = function None -> [] | Some x -> [x] +(* Simple pass doing {x}/v -> /v{x} *) +let elaborate_ipats l = + let rec elab = function + | [] -> [] + | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest + | IPatDispatch p :: rest -> IPatDispatch (List.map elab p) :: elab rest + | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest + | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest + | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ | + IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | + IPatAbstractVars _) as x :: rest -> x :: elab rest + in + elab l + let main ?eqtac ~first_case_is_dispatch ipats = + let ipats = elaborate_ipats ipats in let ip_before, case, ip_after = split_at_first_case ipats in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in - Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) end (* }}} *) @@ -576,7 +588,7 @@ let ssrmovetac = function (tacVIEW_THEN_GRAB view ~conclusion) <*> tclIPAT (IPatClear clr :: ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView view :: IPatClear clr :: ipats) + tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in dgentac <*> tclIPAT (eqmoveipats pat ipats) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 352f88bb3..347a1e4e2 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -412,8 +412,8 @@ let pr_docc = function let pr_ssrdocc _ _ _ = pr_docc ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc -| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ] | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] +| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] END (* Old kinds of terms *) @@ -578,7 +578,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView v -> IPatView (List.map map_ast_closure_term v) + | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat @@ -646,7 +646,7 @@ let interp_ipat ist gl = | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x | IPatTac _ -> assert false (*internal usage only *) @@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats (* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *) | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ] | [ ssrdocc(occ) "->" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, L2R)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]] | [ ssrdocc(occ) "<-" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]] + | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with + | Some [], _ -> [IPatView (true,v)] + | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] + | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ] | [ ssrdocc(occ) ] -> [ match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")] @@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats | [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ] | [ "-/" integer(n) "/" integer (m) "=" ] -> [ [IPatNoop;IPatSimpl(SimplCut(n,m))] ] - | [ ssrfwdview(v) ] -> [ [IPatView v] ] + | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ] | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] END @@ -1154,7 +1160,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id + | { v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1246,7 +1253,8 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") @@ -1676,7 +1684,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt let pr_ssrgen _ _ _ = pr_gen ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen -| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ] +| [ ssrdocc(docc) cpattern(dt) ] -> [ + match docc with + | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here") + | _ -> docc, dt ] | [ cpattern(dt) ] -> [ nodocc, dt ] END diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 11369228c..8f4b2179e 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -107,7 +107,8 @@ let rec pr_ipat p = | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" | IPatAnon One -> str "?" - | IPatView v -> pr_view2 v + | IPatView (false,v) -> pr_view2 v + | IPatView (true,v) -> str"{}" ++ pr_view2 v | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" | IPatTac _ -> str "<tac>" diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 939e97866..7ce2dd64a 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -28,7 +28,6 @@ open Globnames open Stdarg open Genarg open Decl_kinds -open Libnames open Pp open Ppconstr open Printer @@ -143,21 +142,21 @@ END let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f - with _ -> errorstrm (pr_reference f ++ str " is not declared") in + with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> - errorstrm (str "Expected prenex implicits for " ++ pr_reference f) + errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in let impls = match Impargs.implicits_of_global fref with | [cond,impls] -> impls - | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) + | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | _ -> errorstrm (str "Multiple implicits not supported") in match loop impls with | [] -> - errorstrm (str "Expected some implicits for " ++ pr_reference f) + errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] @@ -415,7 +414,7 @@ let interp_search_arg arg = (* Module path postfilter *) -let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m +let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc @@ -433,10 +432,9 @@ GEXTEND Gram END let interp_modloc mr = - let interp_mod (_, mr) = - let {CAst.loc=loc; v=qid} = qualid_of_reference mr in + let interp_mod (_, qid) = try Nametab.full_name_module qid with Not_found -> - CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in + CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b = function | [] -> fun _ _ _ -> true diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index faebe3179..3f974ea06 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -67,9 +67,9 @@ end module State : sig (* View storage API *) - val vsINIT : EConstr.t -> unit tactic - val vsPUSH : (EConstr.t -> EConstr.t tactic) -> unit tactic - val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic + val vsINIT : EConstr.t * Id.t list -> unit tactic + val vsPUSH : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic + val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic val vsASSERT_EMPTY : unit tactic end = struct (* {{{ *) @@ -78,6 +78,7 @@ type vstate = { subject_name : Id.t option; (* top *) (* None if views are being applied to a term *) view : EConstr.t; (* v2 (v1 top) *) + to_clear : Id.t list; } include Ssrcommon.MakeState(struct @@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct let init = None end) -let vsINIT view = tclSET (Some { subject_name = None; view }) +let vsINIT (view, to_clear) = + tclSET (Some { subject_name = None; view; to_clear }) let vsPUSH k = tacUPDATE (fun s -> match s with - | Some { subject_name; view } -> - k view >>= fun view -> - tclUNIT (Some { subject_name; view }) + | Some { subject_name; view; to_clear } -> + k view >>= fun (view, clr) -> + tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr }) | None -> Goal.enter_one ~__LOC__ begin fun gl -> let concl = Goal.concl gl in @@ -102,15 +104,15 @@ let vsPUSH k = | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in let view = EConstr.mkVar id in Ssrcommon.tclINTRO_ID id <*> - k view >>= fun view -> - tclUNIT (Some { subject_name = Some id; view }) + k view >>= fun (view, to_clear) -> + tclUNIT (Some { subject_name = Some id; view; to_clear }) end) let vsCONSUME k = tclGET (fun s -> match s with - | Some { subject_name; view } -> + | Some { subject_name; view; to_clear } -> tclSET None <*> - k subject_name view + k ~name:subject_name view ~to_clear | None -> anomaly "vsCONSUME: empty storage") let vsASSERT_EMPTY = @@ -187,6 +189,16 @@ end * modular, see the 2 functions below that would need to "uncommit" *) let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t +let tclADD_CLEAR_IF_ID (env, ist, t) x = + Ssrprinters.ppdebug (lazy + Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); + let hd, _ = EConstr.decompose_app ist t in + match EConstr.kind ist hd with + | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id]) + | _ -> tclUNIT (x,[]) + +let tclPAIR p x = tclUNIT (x, p) + (* The ssr heuristic : *) (* Estimate a bound on the number of arguments of a raw constr. *) (* This is not perfect, because the unifier may fail to *) @@ -203,14 +215,15 @@ let guess_max_implicits ist glob = (fun _ -> tclUNIT 5) let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal -> - interp_glob ist glob >>= fun (env, sigma, term) -> + interp_glob ist glob >>= fun (env, sigma, term as ot) -> let term_ty = Retyping.get_type_of env sigma term in let ctx, i = Reductionops.splay_prod env sigma term_ty in let rel_ctx = List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in - if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i - then tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) - else Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i) + then Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + else tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) + >>= tclADD_CLEAR_IF_ID ot end (* There are two ways of "applying" a view to term: *) @@ -221,7 +234,7 @@ end (* They require guessing the view hints and the number of *) (* implicits, respectively, which we do by brute force. *) (* Builds v p *) -let interp_view ist v p = +let interp_view ~clear_if_id ist v p = let is_specialize hd = match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in (* We cast the pile of views p into a term p_id *) @@ -230,25 +243,31 @@ let interp_view ist v p = match DAst.get v with | Glob_term.GApp (hd, rargs) when is_specialize hd -> Ssrprinters.ppdebug (lazy Pp.(str "specialize")); - interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr + interp_glob ist (mkGApp p_id rargs) + >>= tclKeepOpenConstr >>= tclPAIR [] | _ -> Ssrprinters.ppdebug (lazy Pp.(str "view")); (* We find out how to build (v p) eventually using an adaptor *) let adaptors = AdaptorDb.(get Forward) in Proofview.tclORELSE - (pad_to_inductive ist v >>= fun vpad -> + (pad_to_inductive ist v >>= fun (vpad,clr) -> Ssrcommon.tclFIRSTa (List.map - (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)) + (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors) + >>= tclPAIR clr) (fun _ -> guess_max_implicits ist v >>= fun n -> Ssrcommon.tclFIRSTi (fun n -> - interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n) - >>= tclKeepOpenConstr + interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n + >>= fun x -> tclADD_CLEAR_IF_ID x x) + >>= fun (ot,clr) -> + if clear_if_id + then tclKeepOpenConstr ot >>= tclPAIR clr + else tclKeepOpenConstr ot >>= tclPAIR [] (* we store in the state (v top), then (v1 (v2 top))... *) -let pile_up_view (ist, v) = +let pile_up_view ~clear_if_id (ist, v) = let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in - State.vsPUSH (fun p -> interp_view ist v p) + State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p) let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> @@ -292,7 +311,7 @@ let pose_proof subject_name p = <*> Tactics.New.reduce_after_refine -let rec apply_all_views ending vs s0 = +let rec apply_all_views ~clear_if_id ending vs s0 = match vs with | [] -> ending s0 | v :: vs -> @@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 = | `Tac tac -> Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); ending s0 <*> Tacinterp.eval_tactic tac <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending vs + Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs | `Term v -> Ssrprinters.ppdebug (lazy Pp.(str"..a term")); - pile_up_view v <*> apply_all_views ending vs s0 + pile_up_view ~clear_if_id v <*> + apply_all_views ~clear_if_id ending vs s0 (* Entry points *********************************************************) -let tclIPAT_VIEWS ~views:vs ~conclusion:tac = +let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac = let end_view_application s0 = - State.vsCONSUME (fun name t -> - finalize_view s0 t >>= pose_proof name <*> - tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in + State.vsCONSUME (fun ~name t ~to_clear -> + let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in + finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id end_view_application vs <*> State.vsASSERT_EMPTY end let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac = let ending_tac s0 = - State.vsCONSUME (fun _ t -> finalize_view s0 ~simple_types t >>= tac) in + State.vsCONSUME (fun ~name:_ t ~to_clear:_ -> + finalize_view s0 ~simple_types t >>= tac) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - State.vsINIT subject <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*> + State.vsINIT (subject,[]) <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id:false ending_tac vs <*> State.vsASSERT_EMPTY end diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index be51fe7f9..b128a95da 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -20,9 +20,11 @@ module AdaptorDb : sig end -(* Apply views to the top of the stack (intro pattern) *) +(* Apply views to the top of the stack (intro pattern). If clear_if_id is + * true (default false) then views that happen to be a variable are considered + * as to be cleared (see the to_clear argument to the continuation) *) val tclIPAT_VIEWS : - views:ast_closure_term list -> + views:ast_closure_term list -> ?clear_if_id:bool -> conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 69d944fa1..9d9b1b2e8 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -131,9 +131,12 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -let isCVar = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false -let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ -> - CErrors.anomaly (str"not a CRef.") +let isCVar = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false +let destCVar = function + | { CAst.v = CRef (qid,_) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> + CErrors.anomaly (str"not a CRef.") let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) | _ -> CErrors.anomaly (str "not a GLambda") @@ -558,8 +561,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when equal u.up_f f -> na - | KpatFixed when equal u.up_f f -> na + | KpatConst when eq_constr_nounivs u.up_f f -> na + | KpatFixed when eq_constr_nounivs u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -579,8 +582,8 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> equal u.up_f f - | KpatFixed -> equal u.up_f f + | KpatConst -> eq_constr_nounivs u.up_f f + | KpatFixed -> eq_constr_nounivs u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f @@ -761,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false) let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> equal u.up_f - | KpatConst -> equal u.up_f + | KpatFixed -> eq_constr_nounivs u.up_f + | KpatConst -> eq_constr_nounivs u.up_f | KpatLam -> fun c -> (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c @@ -1019,8 +1022,10 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern let id_of_cpattern (_, (c1, c2), _) = let open CAst in match DAst.get c1, c2 with - | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x - | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x + | _, Some { v = CRef (qid, _) } when qualid_is_ident qid -> + Some (qualid_basename qid) + | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid -> + Some (qualid_basename qid) | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with |