diff options
Diffstat (limited to 'plugins/ltac')
27 files changed, 455 insertions, 276 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 4cab6ef336..1f628803a3 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -17,6 +17,7 @@ open Refiner open Evd open Locus open Context.Named.Declaration +open Ltac_pretype module NamedDecl = Context.Named.Declaration @@ -27,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma = let filtered = Evd.evar_filtered_env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { - Glob_term.ltac_constrs = constrvars; + ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; @@ -88,7 +89,7 @@ let let_evar name typ = let id = match name with | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in - Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) + Namegen.next_ident_away_in_goal id (Termops.vars_of_env env) | Name.Name id -> id in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 6097951330..89feea8dcf 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -249,7 +249,7 @@ END let pr_by_arg_tac _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t) ARGUMENT EXTEND by_arg_tac TYPED AS tactic_opt diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index b06f35ddc4..00668ddc7d 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -64,7 +64,7 @@ val wit_by_arg_tac : Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : - (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) -> + (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f3f2f27e9e..65c186a419 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true } in - let c = Pretyping.type_uconstr ~flags ist c in + let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac let replace_in_clause_maybe_by ist c1 c2 cl tac = @@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c = (fun c -> tac with_evars (Some (None,ElimOnConstr c))) TACTIC EXTEND simplify_eq - [ "simplify_eq" ] -> [ dEq false None ] -| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ] + [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ] +| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ] END TACTIC EXTEND esimplify_eq -| [ "esimplify_eq" ] -> [ dEq true None ] -| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ] +| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ] +| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ] END let discr_main c = elimOnConstrWithHoles discr_tac false c @@ -117,31 +117,31 @@ let discrHyp id = discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) let injection_main with_evars c = - elimOnConstrWithHoles (injClause None) with_evars c + elimOnConstrWithHoles (injClause None None) with_evars c TACTIC EXTEND injection -| [ "injection" ] -> [ injClause None false None ] -| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ] +| [ "injection" ] -> [ injClause None None false None ] +| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ] END TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause None true None ] -| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ] +| [ "einjection" ] -> [ injClause None None true None ] +| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ] END TACTIC EXTEND injection_as | [ "injection" "as" intropattern_list(ipat)] -> - [ injClause (Some ipat) false None ] + [ injClause None (Some ipat) false None ] | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause (Some ipat)) false c ] + [ mytclWithHoles (injClause None (Some ipat)) false c ] END TACTIC EXTEND einjection_as | [ "einjection" "as" intropattern_list(ipat)] -> - [ injClause (Some ipat) true None ] + [ injClause None (Some ipat) true None ] | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause (Some ipat)) true c ] + [ mytclWithHoles (injClause None (Some ipat)) true c ] END TACTIC EXTEND simple_injection -| [ "simple" "injection" ] -> [ simpleInjClause false None ] -| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ] +| [ "simple" "injection" ] -> [ simpleInjClause None false None ] +| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ] END let injHyp id = @@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c = let flags = { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in - let c = Pretyping.type_uconstr ~flags ~expected_type ist c in + let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in let update = begin fun sigma -> c env sigma end in @@ -403,38 +403,38 @@ open Leminv let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater -VERNAC ARGUMENT EXTEND sort -| [ "Set" ] -> [ GSet ] -| [ "Prop" ] -> [ GProp ] -| [ "Type" ] -> [ GType [] ] -END +(*VERNAC ARGUMENT EXTEND sort_family +| [ "Set" ] -> [ InSet ] +| [ "Prop" ] -> [ InProp ] +| [ "Type" ] -> [ InType ] +END*) VERNAC COMMAND EXTEND DeriveInversionClear -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ] + -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ] END VERNAC COMMAND EXTEND DeriveInversion -| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_tac ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c GProp false inv_tac ] + -> [ add_inversion_lemma_exn na c InProp false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion -| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversionClear -| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ] END @@ -626,19 +626,19 @@ END let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in - let rec substrec = function - | { CAst.v = GVar id } as x -> + let rec substrec x = match DAst.get x with + | GVar id -> if Id.equal id tid then (decr occref; if Int.equal !occref 0 then x else (incr locref; - CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), Misctypes.IntroAnonymous, None))) else x - | c -> map_glob_constr_left_to_right substrec c in + | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t in if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' @@ -646,15 +646,15 @@ let subst_var_with_hole occ tid t = let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in - let rec substrec = function - | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } -> + let rec substrec c = match DAst.get c with + | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; - CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) - | c -> map_glob_constr_left_to_right substrec c + | _ -> map_glob_constr_left_to_right substrec c in substrec t @@ -665,9 +665,9 @@ let hResolve id c occ t = let sigma = Proofview.Goal.sigma gl in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in - let env_ids = Termops.ids_of_context env in - let c_raw = Detyping.detype true env_ids env sigma c in - let t_raw = Detyping.detype true env_ids env sigma t in + let env_ids = Termops.vars_of_env env in + let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in + let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in let rec resolve_hole t_hole = try Pretyping.understand env sigma t_hole @@ -764,7 +764,7 @@ let case_eq_intros_rewrite x = mkCaseEq x; Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let hyps = Tacmach.New.pf_ids_of_hyps gl in + let hyps = Tacmach.New.pf_ids_set_of_hyps gl in let n' = nb_prod (Tacmach.New.project gl) concl in let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in Tacticals.New.tclTHENLIST [ diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 301943a509..5baa0d5c1d 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -48,7 +48,7 @@ let eval_uconstrs ist cs = expand_evars = true } in let map c env sigma = c env sigma in - List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs + List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 2ea0f60ebc..c577cb2198 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -340,7 +340,7 @@ GEXTEND Gram command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l) + Vernacexpr.VernacProof (Some (in_tac ta), l) | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> Vernacexpr.VernacProof (ta,Some l) ] ] @@ -388,16 +388,7 @@ let vernac_solve n info tcom b = p,status) in if not status then Feedback.feedback Feedback.AddedAxiom -let pr_range_selector (i, j) = - if Int.equal i j then int i - else int i ++ str "-" ++ int j - -let pr_ltac_selector = function -| SelectNth i -> int i ++ str ":" -| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" -| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" -| SelectAll -> str "all" ++ str ":" +let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector | [ toplevel_selector(s) ] -> [ s ] @@ -491,6 +482,11 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ] END +VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY +| [ "Locate" "Ltac" reference(r) ] -> + [ Tacentries.print_located_tactic r ] +END + let pr_ltac_ref = Libnames.pr_reference let pr_tacdef_body tacdef_body = diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1a2d895868..fea9e837b1 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -155,6 +155,4 @@ let () = | None -> mt () | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy + Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c874f8d5a3..b148d962ed 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ END let clsubstitute o c = Proofview.Goal.enter begin fun gl -> - let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in + let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun cl -> @@ -195,8 +195,7 @@ let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wi let () = let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in - let printer _ _ _ _ = Pp.str "<Unavailable printer for binders>" in - Pptactic.declare_extra_genarg_pprule wit_binders raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer open Pcoq diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack index 12b4c81fc4..3972b7aac3 100644 --- a/plugins/ltac/ltac_plugin.mlpack +++ b/plugins/ltac/ltac_plugin.mlpack @@ -1,9 +1,9 @@ Tacarg +Tacsubst +Tacenv Pptactic Pltac Taccoerce -Tacsubst -Tacenv Tactic_debug Tacintern Tacentries diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 140cc33440..e467d3e2ca 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -18,7 +18,7 @@ open Geninterp open Stdarg open Tacarg open Libnames -open Ppextend +open Notation_term open Misctypes open Locus open Decl_kinds @@ -116,7 +116,13 @@ type 'a extra_genarg_printer = | Val.Base t -> begin match Val.eq t tag with | None -> default - | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + | Some Refl -> + let open Genprint in + match generic_top_print (in_gen (Topwit wit) x) with + | PrinterBasic pr -> pr () + | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -336,7 +342,7 @@ type 'a extra_genarg_printer = let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn else try - pr_qualid (Nametab.shortest_qualid_of_tactic kn) + pr_qualid (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) str "<" ++ KerName.print kn ++ str ">" @@ -432,12 +438,13 @@ type 'a extra_genarg_printer = let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) - let pr_clauses default_is_concl pr_id = function + (* Some true = default is concl; Some false = default is all; None = no default *) + let pr_clauses has_default pr_id = function | { onhyps=Some []; concl_occs=occs } - when (match default_is_concl with Some true -> true | _ -> false) -> + when (match has_default with Some true -> true | _ -> false) -> pr_with_occurrences mt (occs,()) | { onhyps=None; concl_occs=AllOccurrences } - when (match default_is_concl with Some false -> true | _ -> false) -> mt () + when (match has_default with Some false -> true | _ -> false) -> mt () | { onhyps=None; concl_occs=NoOccurrences } -> pr_in (str " * |-") | { onhyps=None; concl_occs=occs } -> @@ -477,12 +484,14 @@ type 'a extra_genarg_printer = if Int.equal i j then int i else int i ++ str "-" ++ int j - let pr_goal_selector = function - | SelectNth i -> int i ++ str ":" - | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" - | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" - | SelectAll -> str "all" ++ str ":" +let pr_goal_selector toplevel = function + | SelectNth i -> int i ++ str ":" + | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]:" + | SelectAll -> assert toplevel; str "all:" + +let pr_goal_selector ~toplevel s = + (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s let pr_lazy = function | General -> keyword "multi" @@ -662,14 +671,14 @@ type 'a extra_genarg_printer = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) + (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln) ln nal) - [] bll in + Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in - let annot = match names with - | [_] -> + let annot = + if Int.equal (Id.Set.cardinal names) 1 then mt () - | _ -> + else spc() ++ str"{" ++ keyword "struct" ++ spc () ++ pr_id idarg ++ str"}" @@ -988,7 +997,7 @@ type 'a extra_genarg_printer = keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> pr_tac (lcomplete,E) t, lcomplete - | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom + | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> @@ -1040,7 +1049,7 @@ type 'a extra_genarg_printer = let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match ty.CAst.v with + match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in @@ -1172,83 +1181,122 @@ let declare_extra_genarg_pprule wit g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x in let h x = - let env = Global.env () in - h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x + Genprint.PrinterNeedsContext (fun env sigma -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_vernac_genarg_pprule wit f = + let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + Genprint.register_vernac_print0 wit f + (** Registering *) -let run_delayed c = c (Global.env ()) Evd.empty +let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> + let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in + Miscprint.pr_intro_pattern print_constr p) + +let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> + pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, + pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) + +let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + Miscprint.pr_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + pr_with_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, c = match c with + | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) + | clear_flag,ElimOnAnonHyp n as x -> sigma, x + | clear_flag,ElimOnIdent id as x -> sigma, x in + pr_destruction_arg + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) -let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *) - | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g)) - | clear_flag,ElimOnAnonHyp n as x -> x - | clear_flag,ElimOnIdent id as x -> x +let make_constr_printer f c = + Genprint.PrinterNeedsContextAndLevel { + Genprint.default_already_surrounded = Ppconstr.ltop; + Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; + Genprint.printer = (fun env sigma n -> f env sigma n c)} + +let lift f a = Genprint.PrinterBasic (fun () -> f a) let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - let pr_string s = str "\"" ++ str s ++ str "\"" in Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) int; + (pr_or_var int) (pr_or_var int) (lift int); Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) pr_global; + pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); Genprint.register_print0 wit_ident - pr_id pr_id pr_id; + pr_id pr_id (lift pr_id); Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) pr_id; + (pr_located pr_id) (pr_located pr_id) (lift pr_id); Genprint.register_print0 wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c)))); + pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id))) + (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) - Printer.pr_closed_glob + (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) - (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + pr_red_expr_env + ; + Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it))); + pr_bindings_env + ; Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it))); + pr_with_bindings_env + ; + Genprint.register_print0 wit_open_constr_with_bindings + (pr_with_bindings pr_constr_expr pr_lconstr_expr) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + pr_with_bindings_env + ; Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it)); - Genprint.register_print0 Stdarg.wit_int int int int; - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; - Genprint.register_print0 Stdarg.wit_pre_ident str str str; - Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string + pr_destruction_arg_env + ; + Genprint.register_print0 Stdarg.wit_int int int (lift int); + Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); + Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); + Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); + Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) let () = let printer _ _ prtac = prtac (0, E) in diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 0bf9bc7f62..5ecfaf590c 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -16,7 +16,7 @@ open Misctypes open Environ open Constrexpr open Tacexpr -open Ppextend +open Notation_term type 'a grammar_tactic_prod_item_expr = | TacTerm of string @@ -46,6 +46,10 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_vernac_genarg_pprule : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer -> unit + type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { @@ -53,6 +57,8 @@ type pp_tactic = { pptac_prods : grammar_terminals; } +val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t + val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : @@ -67,11 +73,16 @@ val pr_may_eval : val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t + +val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t + val pr_in_clause : ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t -val pr_clauses : bool option -> +val pr_clauses : (* default: *) bool option -> ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t + (* Some true = default is concl; Some false = default is all; None = no default *) val pr_raw_generic : env -> rlevel generic_argument -> Pp.t @@ -91,7 +102,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t val pr_alias : (Val.t -> Pp.t) -> int -> Names.KerName.t -> Val.t list -> Pp.t -val pr_ltac_constant : Nametab.ltac_constant -> Pp.t +val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : raw_tactic_expr -> Pp.t @@ -114,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t val ltop : tolerability + +val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) -> + 'a Genprint.top_printer diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 32494a8793..9ae8bfe65b 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -367,18 +367,30 @@ let do_profile s call_trace tac = let get_local_profiling_results () = List.hd Local.(!stack) -module SM = Map.Make(Stateid.Self) +(* We maintain our own cache of document data, given that the + semantics of the STM implies that synchronized state for opaque + proofs will be lost on QED. This provides some complications later + on as we will have to simulate going back on the document on our + own. *) +module DData = struct + type t = Feedback.doc_id * Stateid.t + let compare x y = Pervasives.compare x y +end + +module SM = Map.Make(DData) let data = ref SM.empty let _ = Feedback.(add_feeder (function - | { id = s; contents = Custom (_, "ltacprof_results", xml) } -> + | { doc_id = d; + span_id = s; + contents = Custom (_, "ltacprof_results", xml) } -> let results = to_ltacprof_results xml in let other_results = (* Multi success can cause this *) - try SM.find s !data + try SM.find (d,s) !data with Not_found -> empty_treenode root in - data := SM.add s (merge_roots results other_results) !data + data := SM.add (d,s) (merge_roots results other_results) !data | _ -> ())) let reset_profile () = @@ -388,7 +400,10 @@ let reset_profile () = (* ******************** *) let print_results_filter ~cutoff ~filter = - let valid id _ = Stm.state_of_id id <> `Expired in + (* The STM doesn't provide yet a proper document query and traversal + API, thus we need to re-check if some states are current anymore + (due to backtracking) using the `state_of_id` API. *) + let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in data := SM.filter valid !data; let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 75b665aad9..1809f0fcdb 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -664,7 +664,7 @@ type rewrite_result = type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *) env : Environ.env ; - unfresh : Id.t list ; (* Unfresh names *) + unfresh : Id.Set.t; (* Unfresh names *) term1 : constr ; ty1 : types ; (* first term and its type (convertible to rew_from) *) cstr : (bool (* prop *) * constr option) ; @@ -1614,7 +1614,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in try let res = - cl_rewrite_clause_aux ?abs strat env [] sigma ty clause + cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> @@ -1884,7 +1884,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context sigma in + let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = @@ -1935,7 +1935,12 @@ let default_morphism sign m = let evars, mor = resolve_one_typeclass env (goalevars evars) morph in mor, proper_projection sigma mor morph +let warn_add_setoid_deprecated = + CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> + Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) + let add_setoid global binders a aeq t n = + warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in @@ -1954,7 +1959,12 @@ let make_tactic name = let tacname = Qualid (Loc.tag tacpath) in TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, []))) +let warn_add_morphism_deprecated = + CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> + Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) + let add_morphism_infer glob m n = + warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 23767c12f5..63e891b455 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -110,7 +110,7 @@ val setoid_transitivity : constr option -> unit Proofview.tactic val apply_strategy : strategy -> Environ.env -> - Names.Id.t list -> + Names.Id.Set.t -> constr -> bool * constr -> evars -> rewrite_result diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9e3a54cc86..4d171ecbc2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -10,7 +10,6 @@ open Util open Names open Term open EConstr -open Pattern open Misctypes open Genarg open Stdarg @@ -18,15 +17,23 @@ open Geninterp exception CannotCoerceTo of string +let base_val_typ wit = + match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.") + let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_context" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (Pptactic.make_constr_printer Printer.pr_econstr_n_env) in wit (* includes idents known to be bound and references *) -let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = +let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_under_binders" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun c -> + Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 1a67f6f888..d7b253a687 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -10,7 +10,6 @@ open Util open Names open EConstr open Misctypes -open Pattern open Genarg open Geninterp @@ -37,8 +36,8 @@ sig val of_constr : constr -> t val to_constr : t -> constr option - val of_uconstr : Glob_term.closed_glob_constr -> t - val to_uconstr : t -> Glob_term.closed_glob_constr option + val of_uconstr : Ltac_pretype.closed_glob_constr -> t + val to_uconstr : t -> Ltac_pretype.closed_glob_constr option val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option @@ -63,9 +62,9 @@ val coerce_to_hint_base : Value.t -> string val coerce_to_int : Value.t -> int -val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders +val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr +val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr @@ -93,4 +92,4 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type -val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type +val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index cf676f598f..ee84be5414 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -63,28 +63,37 @@ let get_separator = function | None -> user_err Pp.(str "Missing separator.") | Some sep -> sep -let rec parse_user_entry s sep = +let check_separator ?loc = function +| None -> () +| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.") + +let rec parse_user_entry ?loc s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry (String.sub s 3 (l-8)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in + check_separator ?loc sep; Ulist1 entry else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in Ulist1sep (entry, get_separator sep) else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + check_separator ?loc sep; Ulist0 entry else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in Ulist0sep (entry, get_separator sep) else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + check_separator ?loc sep; Uopt entry else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in + check_separator ?loc sep; Uentryl ("tactic", n) else + let _ = check_separator ?loc sep in Uentry s let interp_entry_name interp symb = @@ -203,7 +212,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s | TacNonTerm (loc, ((nt, sep), ido)) -> - let symbol = parse_user_entry nt sep in + let symbol = parse_user_entry ?loc nt sep in let interp s = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names @@ -216,7 +225,6 @@ let interp_prod_item = function assert (String.equal s "tactic"); begin match Tacarg.wit_tactic with | ExtraArg tag -> ArgT.Any tag - | _ -> assert false end in let symbol = interp_entry_name interp symbol in @@ -410,7 +418,7 @@ let create_ltac_quotation name cast (e, l) = type tacdef_kind = | NewTac of Id.t - | UpdateTac of Nametab.ltac_constant + | UpdateTac of Tacexpr.ltac_constant let is_defined_tac kn = try ignore (Tacenv.interp_ltac kn); true with Not_found -> false @@ -442,7 +450,7 @@ let register_ltac local tacl = | Tacexpr.TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in let kn = - try Nametab.locate_tactic (snd (qualid_of_reference ident)) + try Tacenv.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> CErrors.user_err ?loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") @@ -465,18 +473,20 @@ let register_ltac local tacl = let defs () = (** Register locally the tactic to handle recursivity. This function affects the whole environment, so that we transactify it afterwards. *) - let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in + let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in let () = List.iter iter_rec recvars in List.map map rfun in - let defs = Future.transactify defs () in + (* STATE XXX: Review what is going on here. Why does this needs + protection? Why is not the STM level protection enough? Fishy *) + let defs = States.with_state_protection defs () in let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> Tacenv.redefine_ltac local kn tac; - let name = Nametab.shortest_qualid_of_tactic kn in + let name = Tacenv.shortest_qualid_of_tactic kn in Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") in List.iter iter defs @@ -489,7 +499,7 @@ let print_ltacs () = let entries = List.sort sort entries in let map (kn, entry) = let qid = - try Some (Nametab.shortest_qualid_of_tactic kn) + try Some (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> None in match qid with @@ -507,6 +517,31 @@ let print_ltacs () = in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) +let locatable_ltac = "Ltac" + +let () = + let open Prettyp in + let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in + let locate_all = Tacenv.locate_extended_all_tactic in + let shortest_qualid = Tacenv.shortest_qualid_of_tactic in + let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in + let print kn = + let qid = qualid_of_path (Tacenv.path_of_tactic kn) in + Tacintern.print_ltac qid + in + let about = name in + register_locatable locatable_ltac { + locate; + locate_all; + shortest_qualid; + name; + print; + about; + } + +let print_located_tactic qid = + Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid) + (** Grammar *) let () = diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index aa8f4efe65..ab2c6b3073 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -62,3 +62,6 @@ 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 +(** Display the absolute name of a tactic. *) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 13b44f0e2c..8c59a36fa6 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -11,6 +11,42 @@ open Pp open Names open Tacexpr +(** Nametab for tactics *) + +(** TODO: Share me somewhere *) +module FullPath = +struct + open Libnames + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (DirPath.repr dir) +end + +module KnTab = Nametab.Make(FullPath)(KerName) + +let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty) + +let push_tactic vis sp kn = + let (tab, revtab) = !tactic_tab in + let tab = KnTab.push vis sp kn tab in + let revtab = KNmap.add kn sp revtab in + tactic_tab := (tab, revtab) + +let locate_tactic qid = KnTab.locate qid (fst !tactic_tab) + +let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab) + +let exists_tactic kn = KnTab.exists kn (fst !tactic_tab) + +let path_of_tactic kn = KNmap.find kn (snd !tactic_tab) + +let shortest_qualid_of_tactic kn = + let sp = KNmap.find kn (snd !tactic_tab) in + KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab) + (** Tactic notations (TacAlias) *) type alias = KerName.t @@ -103,19 +139,19 @@ let replace kn path t = let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Until i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Exactly i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> - let () = Nametab.push_tactic (Until 1) sp kn in + let () = push_tactic (Until 1) sp kn in add kn b t | Some kn0 -> replace kn0 kn t @@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) = let classify_md (local, _, _, _ as o) = Substitute o -let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 958109e5a7..4ecc978fea 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -7,11 +7,21 @@ (************************************************************************) open Names +open Libnames open Tacexpr open Geninterp (** This module centralizes the various ways of registering tactics. *) +(** {5 Tactic naming} *) + +val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit +val locate_tactic : qualid -> ltac_constant +val locate_extended_all_tactic : qualid -> ltac_constant list +val exists_tactic : full_path -> bool +val path_of_tactic : ltac_constant -> full_path +val shortest_qualid_of_tactic : ltac_constant -> qualid + (** {5 Tactic notations} *) type alias = KerName.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 64da097deb..1639736883 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -10,13 +10,14 @@ open Loc open Names open Constrexpr open Libnames -open Nametab open Genredexpr open Genarg open Pattern open Misctypes open Locus +type ltac_constant = KerName.t + type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) @@ -385,7 +386,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map + | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map type ltac_trace = ltac_call_kind Loc.located list diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 0554d43641..f171fd07d7 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -106,19 +106,19 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in - CAst.make @@ GRef (locate_global_with_alias lqid,None), + DAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (CAst.make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[])) + TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) @@ -137,7 +137,7 @@ let intern_isolated_tactic_reference strict ist r = let intern_applied_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - ArgArg (loc,locate_tactic qid) + ArgArg (loc,Tacenv.locate_tactic qid) let intern_applied_tactic_reference ist r = (* An ltac reference *) @@ -264,9 +264,10 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with - | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id) - | c -> clear,ElimOnConstr (c,NoBindings) + let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in + match DAst.get c with + | GVar id -> clear,ElimOnIdent (c.CAst.loc,id) + | _ -> clear,ElimOnConstr ((c, p), NoBindings) else clear,ElimOnIdent (loc,id) @@ -321,13 +322,23 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let dummy_pat = PRel 0 -let intern_typed_pattern ist p = +let intern_typed_pattern ist ~as_type ~ltacvars p = (* we cannot ensure in non strict mode that the pattern is closed *) (* keeping a constr_expr copy is too complicated and we want anyway to *) (* type it, so we remember the pattern as a glob_constr only *) + let metas,pat = + if !strict_check then + let ltacvars = { + Constrintern.ltac_vars = ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in + Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p + else + [], dummy_pat in let (glob,_ as c) = intern_constr_gen true false ist p in let bound_names = Glob_ops.bound_glob_vars glob in - (bound_names,c,dummy_pat) + metas,(bound_names,c,pat) let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = @@ -348,7 +359,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = ltac_extra = ist.extra; } in let c = Constrintern.interp_reference sign r in - match c.CAst.v with + match DAst.get c with | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) | GVar id -> @@ -363,7 +374,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> - Inr (intern_typed_pattern ist c)) + Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c))) (* This seems fairly hacky, but it's the first way I've found to get proper globalization of [unfold]. --adamc *) @@ -528,7 +539,12 @@ let rec intern_atomic lf ist x = then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) | TacChange (Some p,c,cl) -> - TacChange (Some (intern_typed_pattern ist p),intern_constr ist c, + let { ltacvars } = ist in + let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in + let fold accu x = Id.Set.add x accu in + let ltacvars = List.fold_left fold ltacvars metas in + let ist' = { ist with ltacvars } in + TacChange (Some pat,intern_constr ist' c, clause_app (intern_hyp_location ist) cl) (* Equality and inversion *) @@ -721,7 +737,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try - let kn = Nametab.locate_tactic id in + let kn = Tacenv.locate_tactic id in let entries = Tacenv.ltac_entries () in let tac = KNmap.find kn entries in let filter mp = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d3e625e73a..fd75862c6f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -38,6 +38,7 @@ open Tacintern open Taccoerce open Proofview.Notations open Context.Named.Declaration +open Ltac_pretype let ltac_trace_info = Tactic_debug.ltac_trace_info @@ -75,6 +76,9 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) +let base_val_typ wit = + match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") + let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -123,6 +127,8 @@ type tacvalue = let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -139,7 +145,7 @@ let name_vfun appl vle = module TacStore = Geninterp.TacStore -let f_avoid_ids : Id.t list TacStore.field = TacStore.field () +let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field () (* ids inherited from the call context (needed to get fresh ids) *) let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () @@ -230,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = let v = Value.normalize v in - if has_type v (topwit wit_tacvalue) then str "a tactic" - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in - match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr) then - let c = out_gen (topwit wit_constr) v in - match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in + let pr_with_env pr = match env with - | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c - | _ -> str "a term" - else - str "a value of type" ++ spc () ++ pr_argument_type v + | Some (env,sigma) -> pr env sigma + | None -> str "a value of type" ++ spc () ++ pr_argument_type v in + let open Genprint in + match generic_val_print v with + | PrinterBasic pr -> pr () + | PrinterNeedsContext pr -> pr_with_env pr + | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in @@ -501,29 +499,29 @@ let extract_ltac_constr_values ist env = could barely be defined as a feature... *) (* Extract the identifier list from lfun: join all branches (what to do else?)*) -let rec intropattern_ids (loc,pat) = match pat with - | IntroNaming (IntroIdentifier id) -> [id] +let rec intropattern_ids accu (loc,pat) = match pat with + | IntroNaming (IntroIdentifier id) -> Id.Set.add id accu | IntroAction (IntroOrAndPattern (IntroAndPattern l)) -> - List.flatten (List.map intropattern_ids l) + List.fold_left intropattern_ids accu l | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) -> - List.flatten (List.map intropattern_ids (List.flatten ll)) + List.fold_left intropattern_ids accu (List.flatten ll) | IntroAction (IntroInjection l) -> - List.flatten (List.map intropattern_ids l) - | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat + List.fold_left intropattern_ids accu l + | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat | IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _) - | IntroForthcoming _ -> [] + | IntroForthcoming _ -> accu -let extract_ids ids lfun = +let extract_ids ids lfun accu = let fold id v accu = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu - else accu @ intropattern_ids (Loc.tag ipat) + else intropattern_ids accu (Loc.tag ipat) else accu in - Id.Map.fold fold lfun [] + Id.Map.fold fold lfun accu let default_fresh_id = Id.of_string "H" @@ -534,10 +532,10 @@ let interp_fresh_id ist env sigma l = with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with - | None -> [] + | None -> Id.Set.empty | Some l -> l in - let avoid = (extract_ids ids ist.lfun) @ avoid in + let avoid = extract_ids ids ist.lfun avoid in let id = if List.is_empty l then default_fresh_id else @@ -551,7 +549,6 @@ let interp_fresh_id ist env sigma l = (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env sigma = - let open Glob_term in let add_uconstr id v map = try Id.Map.add id (coerce_to_uconstr env v) map with CannotCoerceTo _ -> map @@ -602,10 +599,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = let { closure = constrvars ; term } = interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in let vars = { - Glob_term.ltac_constrs = constrvars.typed; - Glob_term.ltac_uconstrs = constrvars.untyped; - Glob_term.ltac_idents = constrvars.idents; - Glob_term.ltac_genargs = ist.lfun; + ltac_constrs = constrvars.typed; + ltac_uconstrs = constrvars.untyped; + ltac_idents = constrvars.idents; + ltac_genargs = ist.lfun; } in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do @@ -679,8 +676,8 @@ let interp_typed_pattern ist env sigma (_,c,_) = (* Interprets a constr expression *) let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = - try match dest_fun x with - | { CAst.v = GVar id }, _ -> + try match DAst.get (fst (dest_fun x)) with + | GVar id -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -689,7 +686,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = (* dest_fun, List.assoc may raise Not_found *) let sigma, c = interp_fun ist env sigma x in sigma, [c] in - let sigma, l = List.fold_map try_expand_ltac_var sigma l in + let sigma, l = List.fold_left_map try_expand_ltac_var sigma l in sigma, List.flatten l let interp_constr_list ist env sigma c = @@ -818,51 +815,16 @@ let interp_constr_may_eval ist env sigma c = end (** TODO: should use dedicated printers *) -let rec message_of_value v = +let message_of_value v = let v = Value.normalize v in - let open Ftactic in - if has_type v (topwit wit_tacvalue) then - Ftactic.return (str "<tactic>") - else if has_type v (topwit wit_constr) then - let v = out_gen (topwit wit_constr) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c) - end - else if has_type v (topwit wit_unit) then - Ftactic.return (str "()") - else if has_type v (topwit wit_int) then - Ftactic.return (int (out_gen (topwit wit_int) v)) - else if has_type v (topwit wit_intro_pattern) then - let p = out_gen (topwit wit_intro_pattern) v in - let print env sigma c = - let (sigma, c) = c env sigma in - pr_econstr_env env sigma c - in - Ftactic.enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) - end - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end - else if has_type v (topwit wit_uconstr) then - let c = out_gen (topwit wit_uconstr) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_closed_glob_env (pf_env gl) - (project gl) c) - end - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end - else match Value.to_list v with - | Some l -> - Ftactic.List.map message_of_value l >>= fun l -> - Ftactic.return (prlist_with_sep spc (fun x -> x) l) - | None -> - let tag = pr_argument_type v in - Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *) + let pr_with_env pr = + Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in + let open Genprint in + match generic_val_print v with + | PrinterBasic pr -> Ftactic.return (pr ()) + | PrinterNeedsContext pr -> pr_with_env pr + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function | MsgString s -> Ftactic.return (str s) @@ -908,18 +870,18 @@ and interp_intro_pattern_action ist env sigma = function and interp_or_and_intro_pattern ist env sigma = function | IntroAndPattern l -> - let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in + let sigma, l = List.fold_left_map (interp_intro_pattern ist env) sigma l in sigma, IntroAndPattern l | IntroOrPattern ll -> - let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in + let sigma, ll = List.fold_left_map (interp_intro_pattern_list_as_list ist env) sigma ll in sigma, IntroOrPattern ll and interp_intro_pattern_list_as_list ist env sigma = function | [loc,IntroNaming (IntroIdentifier id)] as l -> (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> - List.fold_map (interp_intro_pattern ist env) sigma l) - | l -> List.fold_map (interp_intro_pattern ist env) sigma l + List.fold_left_map (interp_intro_pattern ist env) sigma l) + | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l let interp_intro_pattern_naming_option ist env sigma = function | None -> None @@ -946,13 +908,13 @@ let interp_in_hyp_as ist env sigma (id,ipat) = let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in sigma,(interp_hyp ist env sigma id,ipat) -let interp_binding_name ist sigma = function +let interp_binding_name ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function @@ -964,7 +926,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function let interp_binding ist env sigma (loc,(b,c)) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,(interp_binding_name ist sigma b,c)) + sigma, (loc,(interp_binding_name ist env sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -973,7 +935,7 @@ let interp_bindings ist env sigma = function let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> - let sigma, l = List.fold_map (interp_binding ist env) sigma l in + let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in sigma, ExplicitBindings l let interp_constr_with_bindings ist env sigma (c,bl) = @@ -1043,7 +1005,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else - let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in + let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) @@ -1108,6 +1070,20 @@ let rec read_match_rule lfun ist env sigma = function :: read_match_rule lfun ist env sigma tl | [] -> [] +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None }) + ?(expected_type = WithoutTypeConstraint) ist c = + begin fun env sigma -> + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = Id.Map.empty; + } in + understand_ltac flags env sigma vars expected_type term + end + let warn_deprecated_info = CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated" (fun () -> @@ -1289,7 +1265,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> - let ids = extract_ids [] ist.lfun in + let ids = extract_ids [] ist.lfun Id.Set.empty in let loc_info = (Option.default loc loc',LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in push_trace loc_info ist >>= fun trace -> @@ -1372,15 +1348,25 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = end >>= fun v -> (* No errors happened, we propagate the trace *) let v = append_trace trace v in - Proofview.tclLIFT begin - debugging_step ist - (fun () -> - str"evaluation returns"++fnl()++pr_value None v) + let call_debug env = + Proofview.tclLIFT (debugging_step ist (fun () -> str"evaluation returns"++fnl()++pr_value env v)) in + begin + let open Genprint in + match generic_val_print v with + | PrinterBasic _ -> call_debug None + | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval else Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body))) - | _ -> fail + | (VFun(appl,trace,olfun,[],body)) -> + let extra_args = List.length largs in + Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++ + str (string_of_int extra_args) ++ + str " extra " ++ str (String.plural extra_args "argument") ++ + str ".") + | VRec(_,_) -> fail else fail (* Gives the tactic corresponding to the tactic value *) @@ -1657,7 +1643,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in - let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in + let sigma, cbo = Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma cbo in let named_tac = let tac = Tactics.elim ev keep cb cbo in name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac @@ -1775,7 +1761,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l = - List.fold_map begin fun sigma (c,(ipato,ipats),cls) -> + List.fold_left_map begin fun sigma (c,(ipato,ipats),cls) -> (* TODO: move sigma as a side-effect *) (* spiwack: the [*p] variants are for printing *) let cp = c in @@ -1789,7 +1775,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let l,lp = List.split l in let sigma,el = - Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in + Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma el in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) @@ -1942,7 +1928,7 @@ let interp_tac_gen lfun avoid_ids debug t = (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end -let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t +let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 73e4f3d6ab..5f2723a1e3 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -40,11 +40,11 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } -val f_avoid_ids : Id.t list TacStore.field +val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> - Pattern.constr_under_binders Id.Map.t + Ltac_pretype.constr_under_binders Id.Map.t (** Given an interpretation signature, extract all values which are coercible to a [constr]. *) @@ -54,6 +54,11 @@ val set_debug : debug_info -> unit (** Gives the state of debug *) val get_debug : unit -> debug_info +val type_uconstr : + ?flags:Pretyping.inference_flags -> + ?expected_type:Pretyping.typing_constraint -> + Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open + (** Adds an interpretation function for extra generic arguments *) val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t @@ -74,10 +79,10 @@ val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> - Glob_term.closed_glob_constr + Ltac_pretype.closed_glob_constr val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr -> Glob_term.closed_glob_constr + glob_constr_and_expr -> Ltac_pretype.closed_glob_constr val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr @@ -108,7 +113,7 @@ val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic (** Globalization + interpretation *) -val interp_tac_gen : value Id.Map.t -> Id.t list -> +val interp_tac_gen : value Id.Map.t -> Id.Set.t -> debug_info -> raw_tactic_expr -> unit Proofview.tactic val interp : raw_tactic_expr -> unit Proofview.tactic diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5394b1e116..a669692fc9 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -363,7 +363,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.tag te))) - | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) -> + | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 63b8cc4824..89b78e5907 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -22,7 +22,7 @@ module NamedDecl = Context.Named.Declaration those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Id.Map.t; terms : EConstr.constr Id.Map.t; lhs : 'a; @@ -36,8 +36,8 @@ type 'a t = { (** Some of the functions of {!Matching} return the substitution with a [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces substitution of the former type to the latter. *) -let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map -> - Constr_matching.bound_ident_map * Pattern.extended_patvar_map = +let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> + Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map = fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc) @@ -203,7 +203,7 @@ module PatternMatching (E:StaticEnvironment) = struct let pick l = pick l imatching_error - (** Declares a subsitution, a context substitution and a term substitution. *) + (** Declares a substitution, a context substitution and a term substitution. *) let put subst context terms : unit m = let s = { subst ; context ; terms ; lhs = () } in { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s } diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 01334d36c9..955f8105fb 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -18,7 +18,7 @@ those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Names.Id.Map.t; terms : EConstr.constr Names.Id.Map.t; lhs : 'a; |