aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/g_ltac2.ml4105
-rw-r--r--src/tac2core.ml8
-rw-r--r--src/tac2entries.ml1
-rw-r--r--src/tac2entries.mli1
-rw-r--r--src/tac2qexpr.mli23
-rw-r--r--src/tac2quote.ml79
-rw-r--r--src/tac2quote.mli2
7 files changed, 209 insertions, 10 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index ca3631799b..8c7db71a47 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -30,7 +30,7 @@ let test_lpar_idnum_coloneq =
(match stream_nth 2 strm with
| KEYWORD ":=" -> ()
| _ -> err ())
- | LEFTQMARK ->
+ | KEYWORD "$" ->
(match stream_nth 2 strm with
| IDENT _ ->
(match stream_nth 3 strm with
@@ -40,6 +40,20 @@ let test_lpar_idnum_coloneq =
| _ -> err ())
| _ -> err ())
+(* Hack to recognize "(x)" *)
+let test_lpar_id_rpar =
+ Gram.Entry.of_parser "lpar_id_coloneq"
+ (fun strm ->
+ match stream_nth 0 strm with
+ | KEYWORD "(" ->
+ (match stream_nth 1 strm with
+ | IDENT _ ->
+ (match stream_nth 2 strm with
+ | KEYWORD ")" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
let tac2expr = Tac2entries.Pltac.tac2expr
let tac2type = Gram.entry_create "tactic:tac2type"
let tac2def_val = Gram.entry_create "tactic:tac2def_val"
@@ -291,17 +305,17 @@ open Tac2entries.Pltac
let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
GEXTEND Gram
- GLOBAL: q_ident q_bindings q_intropattern q_intropatterns;
+ GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause;
ident_or_anti:
[ [ id = Prim.ident -> QExpr id
- | LEFTQMARK; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+ | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
] ]
;
q_ident:
[ [ id = ident_or_anti -> Tac2quote.of_anti ~loc:!@loc Tac2quote.of_ident id ] ]
;
simple_binding:
- [ [ "("; LEFTQMARK; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
+ [ [ "("; "$"; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), Tac2quote.of_open_constr ~loc:!@loc c)
| "("; n = Prim.natural; ":="; c = Constr.lconstr; ")" ->
Loc.tag ~loc:!@loc (QExpr (AnonHyp n), Tac2quote.of_open_constr ~loc:!@loc c)
@@ -378,6 +392,89 @@ GEXTEND Gram
q_intropattern:
[ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ~loc:!@loc ipat ] ]
;
+ nat_or_anti:
+ [ [ n = Prim.natural -> QExpr n
+ | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+ ] ]
+ ;
+ eqn_ipat:
+ [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some pat
+ | -> None
+ ] ]
+ ;
+ with_bindings:
+ [ [ "with"; bl = bindings -> bl | -> QNoBindings ] ]
+ ;
+ constr_with_bindings:
+ [ [ c = Constr.constr; l = with_bindings -> (c, l) ] ]
+ ;
+ destruction_arg:
+ [ [ n = Prim.natural -> QElimOnAnonHyp n
+ | (c, bnd) = constr_with_bindings -> QElimOnConstr (c, bnd)
+ ] ]
+ ;
+ as_or_and_ipat:
+ [ [ "as"; ipat = or_and_intropattern -> Some ipat
+ | -> None
+ ] ]
+ ;
+ occs_nums:
+ [ [ nl = LIST1 nat_or_anti -> QOnlyOccurrences nl
+ | "-"; n = nat_or_anti; nl = LIST0 nat_or_anti ->
+ QAllOccurrencesBut (n::nl)
+ ] ]
+ ;
+ occs:
+ [ [ "at"; occs = occs_nums -> occs | -> QAllOccurrences ] ]
+ ;
+ hypident:
+ [ [ id = ident_or_anti ->
+ id,Locus.InHyp
+ | "("; IDENT "type"; IDENT "of"; id = ident_or_anti; ")" ->
+ id,Locus.InHypTypeOnly
+ | "("; IDENT "value"; IDENT "of"; id = ident_or_anti; ")" ->
+ id,Locus.InHypValueOnly
+ ] ]
+ ;
+ hypident_occ:
+ [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
+ ;
+ in_clause:
+ [ [ "*"; occs=occs ->
+ { q_onhyps = None; q_concl_occs = occs }
+ | "*"; "|-"; occs = concl_occ ->
+ { q_onhyps = None; q_concl_occs = occs }
+ | hl = LIST0 hypident_occ SEP ","; "|-"; occs = concl_occ ->
+ { q_onhyps = Some hl; q_concl_occs = occs }
+ | hl = LIST0 hypident_occ SEP "," ->
+ { q_onhyps = Some hl; q_concl_occs = QNoOccurrences }
+ ] ]
+ ;
+ opt_clause:
+ [ [ "in"; cl = in_clause -> Some cl
+ | "at"; occs = occs_nums -> Some { q_onhyps = Some []; q_concl_occs = occs }
+ | -> None
+ ] ]
+ ;
+ concl_occ:
+ [ [ "*"; occs = occs -> occs
+ | -> QNoOccurrences
+ ] ]
+ ;
+ induction_clause:
+ [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
+ cl = opt_clause ->
+ {
+ indcl_arg = c;
+ indcl_eqn = eq;
+ indcl_as = pat;
+ indcl_in = cl;
+ }
+ ] ]
+ ;
+ q_induction_clause:
+ [ [ cl = induction_clause -> Tac2quote.of_induction_clause ~loc:!@loc cl ] ]
+ ;
END
(** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 329c115be3..45fa52ff9b 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -899,6 +899,14 @@ let () = add_scope "intropatterns" begin function
| _ -> scope_fail ()
end
+let () = add_scope "induction_clause" begin function
+| [] ->
+ let scope = Extend.Aentry Tac2entries.Pltac.q_induction_clause in
+ let act tac = tac in
+ Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 52a5899d25..ce86e8aa33 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -28,6 +28,7 @@ let q_ident = Pcoq.Gram.entry_create "tactic:q_ident"
let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
+let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
end
(** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 2e51a4fb2e..1567551246 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -61,4 +61,5 @@ val q_ident : raw_tacexpr Pcoq.Gram.entry
val q_bindings : raw_tacexpr Pcoq.Gram.entry
val q_intropattern : raw_tacexpr Pcoq.Gram.entry
val q_intropatterns : raw_tacexpr Pcoq.Gram.entry
+val q_induction_clause : raw_tacexpr Pcoq.Gram.entry
end
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index b68efe73ac..5075f2d7d4 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -40,3 +40,26 @@ and intro_pattern_action =
and or_and_intro_pattern =
| QIntroOrPattern of intro_pattern list list
| QIntroAndPattern of intro_pattern list
+
+type occurrences =
+| QAllOccurrences
+| QAllOccurrencesBut of int or_anti list
+| QNoOccurrences
+| QOnlyOccurrences of int or_anti list
+
+type hyp_location = (occurrences * Id.t or_anti) * Locus.hyp_location_flag
+
+type clause =
+ { q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
+
+type destruction_arg =
+| QElimOnConstr of Constrexpr.constr_expr * bindings
+| QElimOnIdent of Id.t
+| QElimOnAnonHyp of int
+
+type induction_clause = {
+ indcl_arg : destruction_arg;
+ indcl_eqn : intro_pattern_naming option;
+ indcl_as : or_and_intro_pattern option;
+ indcl_in : clause option;
+}
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index e30acc48ab..9858f611fe 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -36,13 +36,31 @@ let constructor ?loc kn args =
let std_constructor ?loc name args =
constructor ?loc (std_core name) args
+let std_proj ?loc name =
+ AbsKn (std_core name)
+
+let thunk e =
+ let t_unit = coq_core "unit" in
+ let loc = Tac2intern.loc_of_tacexpr e in
+ let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other t_unit), []))] in
+ CTacFun (loc, var, e)
+
let of_pair ?loc (e1, e2) =
let loc = Option.default dummy_loc loc in
CTacApp (loc, CTacCst (loc, AbsKn (Tuple 2)), [e1; e2])
+let of_tuple ?loc el =
+ let loc = Option.default dummy_loc loc in
+ let len = List.length el in
+ CTacApp (loc, CTacCst (loc, AbsKn (Tuple len)), el)
+
let of_int ?loc n =
CTacAtm (Loc.tag ?loc (AtmInt n))
+let of_option ?loc opt = match opt with
+| None -> constructor ?loc (coq_core "None") []
+| Some e -> constructor ?loc (coq_core "Some") [e]
+
let inj_wit ?loc wit x =
let loc = Option.default dummy_loc loc in
CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
@@ -121,17 +139,66 @@ and of_or_and_intro_pattern ?loc = function
and of_intro_patterns ?loc l =
of_list ?loc (List.map (of_intro_pattern ?loc) l)
+let of_hyp_location_flag ?loc = function
+| Locus.InHyp -> std_constructor ?loc "InHyp" []
+| Locus.InHypTypeOnly -> std_constructor ?loc "InHypTypeOnly" []
+| Locus.InHypValueOnly -> std_constructor ?loc "InHypValueOnly" []
+
+let of_occurrences ?loc occ = match occ with
+| QAllOccurrences -> std_constructor ?loc "AllOccurrences" []
+| QAllOccurrencesBut occs ->
+ let map occ = of_anti ?loc of_int occ in
+ let occs = of_list ?loc (List.map map occs) in
+ std_constructor ?loc "AllOccurrencesBut" [occs]
+| QNoOccurrences -> std_constructor ?loc "NoOccurrences" []
+| QOnlyOccurrences occs ->
+ let map occ = of_anti ?loc of_int occ in
+ let occs = of_list ?loc (List.map map occs) in
+ std_constructor ?loc "OnlyOccurrences" [occs]
+
+let of_hyp_location ?loc ((occs, id), flag) =
+ of_tuple ?loc [
+ of_anti ?loc of_ident id;
+ of_occurrences ?loc occs;
+ of_hyp_location_flag ?loc flag;
+ ]
+
+let of_clause ?loc cl =
+ let loc = Option.default dummy_loc loc in
+ let hyps = of_option ~loc (Option.map (fun l -> of_list ~loc (List.map of_hyp_location l)) cl.q_onhyps) in
+ let concl = of_occurrences ~loc cl.q_concl_occs in
+ CTacRec (loc, [
+ std_proj "on_hyps", hyps;
+ std_proj "on_concl", concl;
+ ])
+
+let of_destruction_arg ?loc = function
+| QElimOnConstr (c, bnd) ->
+ let c = of_constr ?loc c in
+ let bnd = of_bindings ?loc bnd in
+ let arg = thunk (of_pair ?loc (c, bnd)) in
+ std_constructor ?loc "ElimOnConstr" [arg]
+| QElimOnIdent id -> std_constructor ?loc "ElimOnIdent" [of_ident ?loc id]
+| QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int ?loc n]
+
+let of_induction_clause ?loc cl =
+ let arg = of_destruction_arg ?loc cl.indcl_arg in
+ let eqn = of_option ?loc (Option.map of_intro_pattern_naming cl.indcl_eqn) in
+ let as_ = of_option ?loc (Option.map of_or_and_intro_pattern cl.indcl_as) in
+ let in_ = of_option ?loc (Option.map of_clause cl.indcl_in) in
+ let loc = Option.default dummy_loc loc in
+ CTacRec (loc, [
+ std_proj "indcl_arg", arg;
+ std_proj "indcl_eqn", eqn;
+ std_proj "indcl_as", as_;
+ std_proj "indcl_in", in_;
+ ])
+
let of_hyp ?loc id =
let loc = Option.default dummy_loc loc in
let hyp = CTacRef (AbsKn (control_core "hyp")) in
CTacApp (loc, hyp, [of_ident ~loc id])
-let thunk e =
- let t_unit = coq_core "unit" in
- let loc = Tac2intern.loc_of_tacexpr e in
- let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other t_unit), []))] in
- CTacFun (loc, var, e)
-
let of_exact_hyp ?loc id =
let loc = Option.default dummy_loc loc in
let refine = CTacRef (AbsKn (control_core "refine")) in
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 4cbe854f75..40ea58e334 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -40,6 +40,8 @@ val of_intro_pattern : ?loc:Loc.t -> intro_pattern -> raw_tacexpr
val of_intro_patterns : ?loc:Loc.t -> intro_pattern list -> raw_tacexpr
+val of_induction_clause : ?loc:Loc.t -> induction_clause -> raw_tacexpr
+
val of_hyp : ?loc:Loc.t -> Id.t -> raw_tacexpr
(** id ↦ 'Control.hyp @id' *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 02:36:40 +0000