diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extraargs.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 131 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 8 | ||||
| -rw-r--r-- | plugins/ltac/pltac.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/pltac.mli | 4 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 72 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 63 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 4 |
10 files changed, 132 insertions, 164 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index ad4374dba3..ff4a82f864 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -41,7 +41,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5) + Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5) (** Backward-compatible tactic notation entry names *) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 6cf5d30a95..c38a4dcd90 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -74,22 +74,22 @@ let hint = G_proofs.hint } GRAMMAR EXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint + GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint tactic_mode constr_may_eval constr_eval toplevel_selector - operconstr; + term; tactic_then_last: - [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> + [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" -> { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) } | -> { [||] } ] ] ; - tactic_then_gen: - [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) } - | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } + for_each_goal: + [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) } + | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) } - | ta = tactic_expr -> { ([ta], None) } - | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) } + | ta = ltac_expr -> { ([ta], None) } + | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) } | -> { ([TacId []], None) } ] ] ; @@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram for [TacExtend] *) [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ] ; - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) } - | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> { + [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } + | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) } + | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> { let (first,tail) = tg in match l , tail with | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) @@ -111,51 +111,51 @@ GRAMMAR EXTEND Gram | false , None -> TacThen (ta0,TacDispatch first) | true , None -> TacThens (ta0,first) } ] | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> { TacTry ta } - | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) } - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) } - | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) } - | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta } - | IDENT "progress"; ta = tactic_expr -> { TacProgress ta } - | IDENT "once"; ta = tactic_expr -> { TacOnce ta } - | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta } - | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta } + [ IDENT "try"; ta = ltac_expr -> { TacTry ta } + | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) } + | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) } + | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) } + | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta } + | IDENT "progress"; ta = ltac_expr -> { TacProgress ta } + | IDENT "once"; ta = ltac_expr -> { TacOnce ta } + | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta } + | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta } (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) } | IDENT "abstract"; tc = NEXT; "using"; s = ident -> { TacAbstract (tc,Some s) } - | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ] + | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) } - | IDENT "tryif" ; ta = tactic_expr ; - "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) } - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ] + [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } + | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) } + | IDENT "tryif" ; ta = ltac_expr ; + "then" ; tat = ltac_expr ; + "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) } + | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } + | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,false,mrl) } | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,true,mrl) } - | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + | b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" -> { TacMatch (b,c,mrl) } - | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst l } - | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacSolve l } | IDENT "idtac"; l = LIST0 message_token -> { TacId l } | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; l = LIST0 message_token -> { TacFail (g,n,l) } | st = simple_tactic -> { st } - | a = tactic_arg -> { TacArg(CAst.make ~loc a) } - | r = reference; la = LIST0 tactic_arg_compat -> + | a = tactic_value -> { TacArg(CAst.make ~loc a) } + | r = reference; la = LIST0 tactic_arg -> { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ] | "0" - [ "("; a = tactic_expr; ")" -> { a } - | "["; ">"; tg = tactic_then_gen; "]" -> { + [ "("; a = ltac_expr; ")" -> { a } + | "["; ">"; tg = for_each_goal; "]" -> { let (tf,tail) = tg in begin match tail with | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) @@ -166,24 +166,24 @@ GRAMMAR EXTEND Gram failkw: [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] ; - (* binder_tactic: level 5 of tactic_expr *) + (* binder_tactic: level 5 of ltac_expr *) binder_tactic: [ RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" -> { TacFun (it,body) } | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] + body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] ; (* Tactic arguments to the right of an application *) - tactic_arg_compat: - [ [ a = tactic_arg -> { a } + tactic_arg: + [ [ a = tactic_value -> { a } | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) } (* Unambiguous entries: tolerated w/o "ltac:" modifier *) | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_arg: + tactic_value: [ [ c = constr_eval -> { ConstrMayEval c } | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l } | IDENT "type_term"; c=uconstr -> { TacPretype c } @@ -223,20 +223,20 @@ GRAMMAR EXTEND Gram | l = ident -> { Name.Name l } ] ] ; let_clause: - [ [ idr = identref; ":="; te = tactic_expr -> + [ [ idr = identref; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr te) } - | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr -> + | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr -> { (na, arg_of_expr te) } - | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> + "["; pc = Constr.cpattern; "]" -> { Subterm (oid, pc) } - | pc = Constr.lconstr_pattern -> { Term pc } ] ] + | pc = Constr.cpattern -> { Term pc } ] ] ; - match_hyps: + match_hyp: [ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) } | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) } | na = name; ":="; mpv = match_pattern -> @@ -250,19 +250,19 @@ GRAMMAR EXTEND Gram ] ] ; match_context_rule: - [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_context_list: [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl } | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ] ; match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_list: [ [ mrl = LIST1 match_rule SEP "|" -> { mrl } @@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; - redef = ltac_def_kind; body = tactic_expr -> + redef = ltac_def_kind; body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) } | name = Constr.global; redef = ltac_def_kind; - body = tactic_expr -> + body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram ] ] ; tactic: - [ [ tac = tactic_expr -> { tac } ] ] + [ [ tac = ltac_expr -> { tac } ] ] ; range_selector: @@ -314,15 +314,12 @@ GRAMMAR EXTEND Gram { let open Goal_select in Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] ; - selector_body: + selector: [ [ l = range_selector_or_nth -> { l } | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] ; - selector: - [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ] - ; toplevel_selector: - [ [ sel = selector_body; ":" -> { sel } + [ [ sel = selector; ":" -> { sel } | "!"; ":" -> { Goal_select.SelectAlreadyFocused } | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] ; @@ -343,8 +340,8 @@ GRAMMAR EXTEND Gram tac = Pltac.tactic -> { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; - operconstr: LEVEL "0" - [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> + term: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" -> { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] ; @@ -402,7 +399,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in ComTactic.solve g ~info t ~with_end_tac } END @@ -415,7 +412,7 @@ VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof VtProofStep{ proof_block_detection = pbr } } -> { let t, abstract = rm_abstract t in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in ComTactic.solve_parallel ~info t ~abstract ~with_end_tac } END diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index c186a83a5c..97d75261c5 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram ; simple_intropattern: [ [ pat = simple_intropattern_closed; - l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] -> + l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] -> { let {CAst.loc=loc0;v=pat} = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in @@ -320,7 +320,7 @@ GRAMMAR EXTEND Gram with_bindings: [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ] ; - red_flags: + red_flag: [ [ IDENT "beta" -> { [FBeta] } | IDENT "iota" -> { [FMatch;FFix;FCofix] } | IDENT "match" -> { [FMatch] } @@ -337,7 +337,7 @@ GRAMMAR EXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) } + [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) } | d = delta_flag -> { all_with d } ] ] ; @@ -460,7 +460,7 @@ GRAMMAR EXTEND Gram [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ] ; by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac } + [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac } | -> { None } ] ] ; rewriter : diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index b7b54143df..94e398fe5d 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -37,8 +37,10 @@ let clause_dft_concl = (* Main entries for ltac *) -let tactic_arg = Entry.create "tactic_arg" -let tactic_expr = Entry.create "tactic_expr" +let tactic_value = Entry.create "tactic_value" +let tactic_arg = tactic_value +let ltac_expr = Entry.create "ltac_expr" +let tactic_expr = ltac_expr let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 8565c4b4d6..3a4a081c93 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -31,8 +31,12 @@ val simple_tactic : raw_tactic_expr Entry.t val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t val in_clause : Names.lident Locus.clause_expr Entry.t val clause_dft_concl : Names.lident Locus.clause_expr Entry.t +val tactic_value : raw_tactic_arg Entry.t val tactic_arg : raw_tactic_arg Entry.t + [@@deprecated "Deprecated in 8.13; use 'tactic_value' instead"] +val ltac_expr : raw_tactic_expr Entry.t val tactic_expr : raw_tactic_expr Entry.t + [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"] val binder_tactic : raw_tactic_expr Entry.t val tactic : raw_tactic_expr Entry.t val tactic_eoi : raw_tactic_expr Entry.t diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 6a9fb5c2ea..5e199dad62 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** This module implements pretty-printers for tactic_expr syntactic +(** This module implements pretty-printers for ltac_expr syntactic objects and their subcomponents. *) open Genarg diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5ef76dbdc1..a1970cbce2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation -let resolve_subrelation env avoid car rel sort prf rel' res = +let resolve_subrelation env car rel sort prf rel' res = if Termops.eq_constr (fst res.rew_evars) rel rel' then res else let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in @@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res = rew_prf = RewPrf (rel', appsub); rew_evars = evars } -let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars = +let resolve_morphism env m args args' (b,cstr) evars = let evars, morph_instance, proj, sigargs, m', args, args' = let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with | Some i -> i @@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let proof = applist (proj, List.rev projargs) in let newt = applist (m', List.rev typeargs) in match respars with - [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt + [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt | _ -> assert(false) -let apply_constraint env avoid car rel prf cstr res = +let apply_constraint env car rel prf cstr res = match snd cstr with | None -> res - | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res + | Some r -> resolve_subrelation env car rel (fst cstr) prf r res -let coerce env avoid cstr res = +let coerce env cstr res = let evars, (rel, prf) = get_rew_prf res.rew_evars res in let res = { res with rew_evars = evars } in - apply_constraint env avoid res.rew_car rel prf cstr res + apply_constraint env res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = let (nowhere_except_in,occs) = convert_occs loccs in @@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy = then List.mem occ occs else not (List.mem occ occs) in - { strategy = fun { state = occ ; env ; unfresh ; + { strategy = fun { state = occ ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> let unif = if isEvar (goalevars evars) t then None else unify env evars t in match unif with @@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let res = Success (coerce env unfresh cstr res) in + let res = Success (coerce env cstr res) in (occ, res) } @@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c = let unfold_match env sigma sk app = match EConstr.kind sigma app with - | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> + | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in Reductionops.whd_beta env sigma (mkApp (v, args)) @@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | None -> false | Some r -> not (is_rew_cast r.rew_prf)) args' then - let evars', prf, car, rel, c1, c2 = - resolve_morphism env unfresh t m args args' (prop, cstr') evars' + let evars', prf, car, rel, c2 = + resolve_morphism env m args args' (prop, cstr') evars' in - let res = { rew_car = ty; rew_from = c1; + let res = { rew_car = ty; rew_from = t; rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = evars' } in Success res @@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let res = match prf with | RewPrf (rel, prf) -> - Success (apply_constraint env unfresh res.rew_car + Success (apply_constraint env res.rew_car rel prf (prop,cstr) res) | _ -> Success res in state, res @@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> res in state, res - (* if x' = None && flags.under_lambdas then *) - (* let lam = mkLambda (n, x, b) in *) - (* let lam', occ = aux env lam occ None in *) - (* let res = *) - (* match lam' with *) - (* | None -> None *) - (* | Some (prf, (car, rel, c1, c2)) -> *) - (* Some (resolve_morphism env sigma t *) - (* ~fnewt:unfold_all *) - (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *) - (* cstr evars) *) - (* in res, occ *) - (* else *) - | Prod (n, dom, codom) -> let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = @@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing dependent relations and using projections to get them out. *) - (* | Lambda (n, t, b) when flags.under_lambdas -> *) - (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *) - (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *) - (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *) - (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *) - (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *) - (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *) - (* (match b' with *) - (* | Some (Some r) -> *) - (* let prf = match r.rew_prf with *) - (* | RewPrf (rel, prf) -> *) - (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *) - (* let prf = mkLambda (n', t, prf) in *) - (* RewPrf (rel, prf) *) - (* | x -> x *) - (* in *) - (* Some (Some { r with *) - (* rew_prf = prf; *) - (* rew_car = mkProd (n, t, r.rew_car); *) - (* rew_from = mkLambda(n, t, r.rew_from); *) - (* rew_to = mkLambda (n, t, r.rew_to) }) *) - (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in + let unfresh = match n'.binder_name with + | Anonymous -> unfresh + | Name id -> Id.Set.add id unfresh + in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in @@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Success r -> let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in let res = make_leibniz_proof env case ty r in - state, Success (coerce env unfresh (prop,cstr) res) + state, Success (coerce env (prop,cstr) res) | Fail | Identity -> if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in @@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> Success (coerce env unfresh (prop,cstr) r) + | Success r -> Success (coerce env (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index d58a76fe13..a05b36c1b4 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -31,21 +31,9 @@ type argument = Genarg.ArgT.any Extend.user_symbol (**********************************************************************) (* Interpret entry names of the form "ne_constr_list" as entry keys *) -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := Int.equal c d; - incr i - done; - !break - let atactic n = if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic - else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n) + else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name @@ -70,28 +58,37 @@ let check_separator ?loc = function | 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 ?loc (String.sub s 3 (l-8)) None in + let open CString in + let matches pre suf s = + String.length s > (String.length pre + String.length suf) && + is_prefix pre s && is_suffix suf s + in + let basename pre suf s = + let plen = String.length pre in + String.sub s plen (String.length s - (plen + String.length suf)) + in + let tactic_len = String.length "tactic" in + if matches "ne_" "_list" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list" s) 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 ?loc (String.sub s 3 (l-12)) None in + else if matches "ne_" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in Ulist1sep (entry, get_separator sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + else if matches "" "_list" s then + let entry = parse_user_entry ?loc (basename "" "_list" s) None in check_separator ?loc sep; Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in + else if matches "" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in Ulist0sep (entry, get_separator sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + else if matches "" "_opt" s then + let entry = parse_user_entry ?loc (basename "" "_opt" s) 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 + else if String.length s = tactic_len + 1 && is_prefix "tactic" s + && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then + let n = Char.code s.[tactic_len] - Char.code '0' in check_separator ?loc sep; Uentryl ("tactic", n) else @@ -119,7 +116,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) + Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) @@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in - assert (coincide (ArgT.repr tag) "tactic" 0); + assert (CString.is_suffix "tactic" (ArgT.repr tag)); get_tacentry n lev (** Tactic grammar extensions *) @@ -386,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods = in List.iteri iter (List.rev prods); (* We call [extend_atomic_tactic] only for "basic tactics" (the ones - at tactic_expr level 0) *) + at ltac_expr level 0) *) if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) @@ -423,7 +420,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Pcoq.Production.make rule action]) in - Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]} + Pcoq.grammar_extend Pltac.tactic_value {pos=None; data=[gram]} (** Command *) @@ -558,10 +555,10 @@ let print_located_tactic qid = let () = let entries = [ - AnyEntry Pltac.tactic_expr; + AnyEntry Pltac.ltac_expr; AnyEntry Pltac.binder_tactic; AnyEntry Pltac.simple_tactic; - AnyEntry Pltac.tactic_arg; + AnyEntry Pltac.tactic_value; ] in register_grammars_by_name "tactic" entries diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 12bfb4d09e..7728415ddd 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1997,7 +1997,7 @@ let interp_tac_gen lfun avoid_ids debug t = let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t (* MUST be marshallable! *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } @@ -2019,7 +2019,7 @@ let hide_interp {global;ast} = hide_interp (Proofview.Goal.env gl) end -let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp +let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp (***************************************************************************) (** Register standard arguments *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 01d7306c9d..fe3079198c 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -126,12 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t -> val interp : raw_tactic_expr -> unit Proofview.tactic (** Hides interpretation for pretty-print *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } -val hide_interp : tactic_expr ComTactic.tactic_interpreter +val hide_interp : ltac_expr -> ComTactic.interpretable (** Internals that can be useful for syntax extensions. *) |