aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_tactic.ml451
-rw-r--r--parsing/ppconstr.ml14
-rw-r--r--parsing/ppconstr.mli2
-rw-r--r--parsing/pptactic.ml25
-rw-r--r--parsing/q_coqast.ml413
5 files changed, 61 insertions, 44 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5ab401550..bea3929df 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -162,6 +162,10 @@ let mkCLambdaN_simple bl c =
let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in
mkCLambdaN_simple_loc loc bl c
+let map_int_or_var f = function
+ | Rawterm.ArgArg x -> Rawterm.ArgArg (f x)
+ | Rawterm.ArgVar _ as y -> y
+
(* Auxiliary grammar rules *)
GEXTEND Gram
@@ -173,6 +177,10 @@ GEXTEND Gram
[ [ n = integer -> Rawterm.ArgArg n
| id = identref -> Rawterm.ArgVar id ] ]
;
+ nat_or_var:
+ [ [ n = natural -> Rawterm.ArgArg n
+ | id = identref -> Rawterm.ArgVar id ] ]
+ ;
(* An identifier or a quotation meta-variable *)
id_or_meta:
[ [ id = identref -> AI id
@@ -203,18 +211,22 @@ GEXTEND Gram
;
conversion:
[ [ c = constr -> (None, c)
- | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
- | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr ->
- (Some (nl,c1), c2) ] ]
+ | c1 = constr; "with"; c2 = constr -> (Some (all_occurrences_expr,c1),c2)
+ | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
+ (Some (occs,c1), c2) ] ]
;
smart_global:
[ [ c = global -> AN c
| s = ne_string -> ByNotation (loc,s) ] ]
;
+ occs_nums:
+ [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl
+ | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
+ (* have used int_or_var instead of nat_or_var for compatibility *)
+ all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ]
+ ;
occs:
- [ [ "at"; nl = LIST1 integer -> List.map (fun x -> Rawterm.ArgArg x) nl
- | "at"; id = identref -> [Rawterm.ArgVar id]
- | -> [] ] ]
+ [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr_but [] ] ]
;
pattern_occ:
[ [ c = constr; nl = occs -> (nl,c) ] ]
@@ -323,29 +335,29 @@ GEXTEND Gram
;
in_clause:
[ [ "*"; occs=occs ->
- {onhyps=None; onconcl=true; concl_occs=occs}
- | "*"; "|-"; (b,occs)=concl_occ ->
- {onhyps=None; onconcl=b; concl_occs=occs}
- | hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ ->
- {onhyps=Some hl; onconcl=b; concl_occs=occs}
+ {onhyps=None; concl_occs=occs}
+ | "*"; "|-"; occs=concl_occ ->
+ {onhyps=None; concl_occs=occs}
+ | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
+ {onhyps=Some hl; concl_occs=occs}
| hl=LIST0 hypident_occ SEP"," ->
- {onhyps=Some hl; onconcl=false; concl_occs=[]} ] ]
+ {onhyps=Some hl; concl_occs=no_occurrences_expr} ] ]
;
clause_dft_concl:
[ [ "in"; cl = in_clause -> cl
- | occs=occs -> {onhyps=Some[]; onconcl=true; concl_occs=occs}
- | -> {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ]
+ | occs=occs -> {onhyps=Some[]; concl_occs=occs}
+ | -> {onhyps=Some[]; concl_occs=all_occurrences_expr} ] ]
;
clause_dft_all:
[ [ "in"; cl = in_clause -> cl
- | -> {onhyps=None; onconcl=true; concl_occs=[]} ] ]
+ | -> {onhyps=None; concl_occs=all_occurrences_expr} ] ]
;
opt_clause:
[ [ "in"; cl = in_clause -> Some cl | -> None ] ]
;
concl_occ:
- [ [ "*"; occs = occs -> (true,occs)
- | -> (false, []) ] ]
+ [ [ "*"; occs = occs -> occs
+ | -> no_occurrences_expr ] ]
;
simple_clause:
[ [ "in"; idl = LIST1 id_or_meta -> idl
@@ -493,9 +505,10 @@ GEXTEND Gram
| IDENT "cut"; c = constr -> TacCut c
| IDENT "generalize"; c = constr ->
- TacGeneralize [(([],c),Names.Anonymous)]
+ TacGeneralize [((all_occurrences_expr,c),Names.Anonymous)]
| IDENT "generalize"; c = constr; l = LIST1 constr ->
- TacGeneralize (List.map (fun c -> (([],c),Names.Anonymous)) (c::l))
+ let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in
+ TacGeneralize (List.map gen_everywhere (c::l))
| IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs;
na = as_name;
l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 0f0c38adc..04b700236 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -674,10 +674,16 @@ let pr_cases_pattern_expr = pr_patt ltop
let pr_binders = pr_undelimited_binders (pr ltop)
-let pr_with_occurrences pr = function
- ([],c) -> pr c
- | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++
- hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+let pr_with_occurrences_with_trailer pr occs trailer =
+ match occs with
+ ((false,[]),c) -> pr c ++ trailer
+ | ((nowhere_except_in,nl),c) ->
+ hov 1 (pr c ++ spc() ++ str"at " ++
+ (if nowhere_except_in then mt() else str "- ") ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl) ++ trailer)
+
+let pr_with_occurrences pr occs =
+ pr_with_occurrences_with_trailer pr occs (mt())
let pr_red_flag pr r =
(if r.rBeta then pr_arg str "beta" else mt ()) ++
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index f351144dc..83339ee2f 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -55,6 +55,8 @@ val pr_qualid : qualid -> std_ppcmds
val pr_with_occurrences :
('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
+val pr_with_occurrences_with_trailer :
+ ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds -> std_ppcmds
val pr_red_expr :
('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
('a,'b) red_expr_gen -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c0dbc0eff..e59df48aa 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -417,14 +417,14 @@ let pr_simple_clause pr_id = function
| l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
let pr_clauses pr_id = function
- { onhyps=None; onconcl=true; concl_occs=nl } ->
- pr_in (pr_with_occurrences (fun () -> str " *") (nl,()))
- | { onhyps=None; onconcl=false } -> pr_in (str " * |-")
- | { onhyps=Some l; onconcl=true; concl_occs=nl } ->
- pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l
- ++ pr_with_occurrences (fun () -> str" |- *") (nl,()))
- | { onhyps=Some l; onconcl=false } ->
- pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l)
+ | { onhyps=None; concl_occs=occs } ->
+ if occs = no_occurrences_expr then pr_in (str " * |-")
+ else pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
+ | { onhyps=Some l; concl_occs=occs } ->
+ pr_in
+ (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++
+ (if occs = no_occurrences_expr then mt ()
+ else pr_with_occurrences (fun () -> str" |- *") (occs,())))
let pr_clause_pattern pr_id = function
| (None, []) -> mt ()
@@ -829,12 +829,9 @@ and pr_atom1 = function
hov 1 (str "change" ++ brk (1,1) ++
(match occ with
None -> mt()
- | Some([],c1) -> hov 1 (pr_constr c1 ++ spc() ++ str "with ")
- | Some(ocl,c1) ->
- hov 1 (pr_constr c1 ++ spc() ++
- str "at " ++ prlist_with_sep spc (pr_or_var int) ocl) ++
- spc() ++
- str "with ") ++
+ | Some occlc ->
+ pr_with_occurrences_with_trailer pr_constr occlc
+ (spc () ++ str "with ")) ++
pr_constr c ++ pr_clauses pr_ident h)
(* Equivalence relations *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 5c31fcee6..4b52772b5 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -95,7 +95,9 @@ let mlexpr_of_or_var f = function
let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
-let mlexpr_of_occs = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)
+let mlexpr_of_occs =
+ mlexpr_of_pair
+ mlexpr_of_bool (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int))
let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
@@ -111,7 +113,6 @@ let mlexpr_of_clause cl =
<:expr< {Tacexpr.onhyps=
$mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location)
cl.Tacexpr.onhyps$;
- Tacexpr.onconcl= $mlexpr_of_bool cl.Tacexpr.onconcl$;
Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >>
let mlexpr_of_red_flags {
@@ -165,8 +166,7 @@ let rec mlexpr_of_constr = function
| _ -> failwith "mlexpr_of_constr: TODO"
let mlexpr_of_occ_constr =
- mlexpr_of_pair (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int))
- mlexpr_of_constr
+ mlexpr_of_occurrences mlexpr_of_constr
let mlexpr_of_red_expr = function
| Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >>
@@ -177,9 +177,8 @@ let mlexpr_of_red_expr = function
| Rawterm.Lazy f ->
<:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >>
| Rawterm.Unfold l ->
- let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in
- let f2 = mlexpr_of_by_notation mlexpr_of_reference in
- let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in
+ let f1 = mlexpr_of_by_notation mlexpr_of_reference in
+ let f = mlexpr_of_list (mlexpr_of_occurrences f1) in
<:expr< Rawterm.Unfold $f l$ >>
| Rawterm.Fold l ->
<:expr< Rawterm.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 07:34:32 +0000