aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml5
-rw-r--r--plugins/funind/gen_principle.ml15
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml29
-rw-r--r--plugins/funind/recdef.ml20
5 files changed, 56 insertions, 17 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f2658a395f..743afe4177 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -645,6 +645,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
match EConstr.kind sigma f with
| Int _ -> user_err Pp.(str "integer cannot be applied")
| Float _ -> user_err Pp.(str "float cannot be applied")
+ | Array _ -> user_err Pp.(str "array cannot be applied")
| App _ ->
assert false (* we have collected all the app in decompose_app *)
| Proj _ -> assert false (*FIXME*)
@@ -696,6 +697,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
; build_proof do_finalize new_infos ]
g
| Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
+ | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet")
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
Indfun_common.observe_tac
@@ -862,7 +864,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index f773157c52..45b1713441 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -103,6 +103,8 @@ let is_rec names =
names nal)
b
| GApp (f, args) -> List.exists (lookup names) (f :: args)
+ | GArray (_u, t, def, ty) ->
+ Array.exists (lookup names) t || lookup names def || lookup names ty
| GCases (_, _, el, brl) ->
List.exists (fun (e, _) -> lookup names e) el
|| List.exists (lookup_br names) brl
@@ -1524,9 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let lemma =
fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
in
- let (_ : GlobRef.t list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ let (_ : _ list) =
+ Declare.Proof.save_regular ~proof:lemma
+ ~opaque:Vernacexpr.Transparent ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
@@ -1597,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
lemma)
in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma
+ ~opaque:Vernacexpr.Transparent ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
@@ -2047,7 +2049,8 @@ let rec add_args id new_args =
| CGeneralization _ ->
CErrors.anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ ->
- CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters."))
+ CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+ | CArray _ -> CErrors.anomaly ~label:"add_args " (Pp.str "CArray."))
let rec get_args b t :
Constrexpr.local_binder_expr list
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 11e4fa0ac7..6ed61043f9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -568,6 +568,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
| GProd _ -> user_err Pp.(str "Cannot apply a type")
| GInt _ -> user_err Pp.(str "Cannot apply an integer")
| GFloat _ -> user_err Pp.(str "Cannot apply a float")
+ | GArray _ -> user_err Pp.(str "Cannot apply an array")
(* end of the application treatement *) )
| GLambda (n, _, t, b) ->
(* we first compute the list of constructor
@@ -672,6 +673,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
build_entry_lc env sigma funnames avoid match_expr
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast (b, _) -> build_entry_lc env sigma funnames avoid b
+ | GArray _ -> user_err Pp.(str "Not handled GArray")
and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples)
(brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return =
@@ -1196,7 +1198,7 @@ let rec compute_cst_params relnames params gt =
discrimination ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GArray _ ->
CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case"))
gt
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5026120849..8e1331ace9 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,7 +109,13 @@ let change_vars =
| GCast (b, c) ->
GCast
( change_vars mapping b
- , Glob_ops.map_cast_type (change_vars mapping) c ))
+ , Glob_ops.map_cast_type (change_vars mapping) c )
+ | GArray (u, t, def, ty) ->
+ GArray
+ ( u
+ , Array.map (change_vars mapping) t
+ , change_vars mapping def
+ , change_vars mapping ty ))
rt
and change_vars_br mapping ({CAst.loc; v = idl, patl, res} as br) =
let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -282,6 +288,12 @@ let rec alpha_rt excluded rt =
GCast (alpha_rt excluded b, Glob_ops.map_cast_type (alpha_rt excluded) c)
| GApp (f, args) ->
GApp (alpha_rt excluded f, List.map (alpha_rt excluded) args)
+ | GArray (u, t, def, ty) ->
+ GArray
+ ( u
+ , Array.map (alpha_rt excluded) t
+ , alpha_rt excluded def
+ , alpha_rt excluded ty )
in
new_rt
@@ -331,7 +343,9 @@ let is_free_in id =
| GHole _ -> false
| GCast (b, (CastConv t | CastVM t | CastNative t)) ->
is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b
- | GInt _ | GFloat _ -> false)
+ | GInt _ | GFloat _ -> false
+ | GArray (_u, t, def, ty) ->
+ Array.exists is_free_in t || is_free_in def || is_free_in ty)
x
and is_free_in_br {CAst.v = ids, _, rt} =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -404,6 +418,12 @@ let replace_var_by_term x_id term =
| (GSort _ | GHole _) as rt -> rt
| GInt _ as rt -> rt
| GFloat _ as rt -> rt
+ | GArray (u, t, def, ty) ->
+ GArray
+ ( u
+ , Array.map replace_var_by_pattern t
+ , replace_var_by_pattern def
+ , replace_var_by_pattern ty )
| GCast (b, c) ->
GCast
( replace_var_by_pattern b
@@ -510,7 +530,10 @@ let expand_as =
( sty
, Option.map (expand_as map) po
, List.map (fun (rt, t) -> (expand_as map rt, t)) el
- , List.map (expand_as_br map) brl ))
+ , List.map (expand_as_br map) brl )
+ | GArray (u, t, def, ty) ->
+ GArray
+ (u, Array.map (expand_as map) t, expand_as map def, expand_as map ty))
and expand_as_br map {CAst.loc; v = idl, cpl, rt} =
CAst.make ?loc (idl, cpl, expand_as (List.fold_left add_as map cpl) rt)
in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 701ea56c2a..253c95fa67 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -59,7 +59,8 @@ let declare_fun name kind ?univs value =
let defined lemma =
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
()
@@ -305,9 +306,11 @@ let check_not_nested env sigma forbidden e =
| Lambda (_, t, b) -> check_not_nested t; check_not_nested b
| LetIn (_, v, t, b) ->
check_not_nested t; check_not_nested b; check_not_nested v
- | App (f, l) ->
- check_not_nested f;
- Array.iter check_not_nested l
+ | App (f, l) -> check_not_nested f
+ | Array (_u, t, def, ty) ->
+ Array.iter check_not_nested t;
+ check_not_nested def;
+ check_not_nested ty
| Proj (p, c) -> check_not_nested c
| Const _ -> ()
| Ind _ -> ()
@@ -447,6 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
match EConstr.kind sigma expr_info.info with
| CoFix _ | Fix _ ->
user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
+ | Array _ -> user_err Pp.(str "Function cannot treat arrays")
| Proj _ -> user_err Pp.(str "Function cannot treat projections")
| LetIn (na, b, t, e) ->
let new_continuation_tac =
@@ -1500,7 +1504,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
in
let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
in
()
in
@@ -1659,7 +1663,11 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
in
let _ =
Flags.silently
- (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
+ (fun () ->
+ let (_ : _ list) =
+ Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
+ in
+ ())
()
in
()
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:28:39 +0000