aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml9
-rw-r--r--plugins/funind/gen_principle.ml19
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml29
-rw-r--r--plugins/funind/recdef.ml43
5 files changed, 75 insertions, 29 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9b578d4697..743afe4177 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -585,10 +585,10 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
let sigma = project g in
(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
match EConstr.kind sigma dyn_infos.info with
- | Case (ci, ct, t, cb) ->
+ | Case (ci, ct, iv, t, cb) ->
let do_finalize_t dyn_info' g =
let t = dyn_info'.info in
- let dyn_infos = {dyn_info' with info = mkCase (ci, ct, t, cb)} in
+ let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in
let g_nb_prod = nb_prod (project g) (pf_concl g) in
let g, type_of_term = tac_type_of g t in
let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in
@@ -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 dcca694200..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
@@ -987,7 +989,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
( UnivGen.constr_of_monomorphic_global
@@ Coqlib.lib_ref "core.False.type" )) ->
Proofview.V82.of_tactic tauto g
- | Case (_, _, v, _) ->
+ | Case (_, _, _, v, _) ->
tclTHENLIST
[Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite]
g
@@ -1026,7 +1028,7 @@ let rec reflexivity_with_destruct_cases g =
match
EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2)
with
- | Case (_, _, v, _) ->
+ | Case (_, _, _, v, _) ->
tclTHENLIST
[ Proofview.V82.of_tactic (simplest_case v)
; Proofview.V82.of_tactic intros
@@ -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 884792cc15..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,14 +306,16 @@ 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 _ -> ()
| Construct _ -> ()
- | Case (_, t, e, a) ->
+ | Case (_, t, _, e, a) ->
check_not_nested t;
check_not_nested e;
Array.iter check_not_nested a
@@ -374,7 +377,13 @@ type journey_info =
; lambdA : (Name.t * types * constr, constr) journey_info_tac
; casE :
((constr infos -> tactic) -> constr infos -> tactic)
- -> (case_info * constr * constr * constr array, constr) journey_info_tac
+ -> ( case_info
+ * constr
+ * (constr, EInstance.t) case_invert
+ * constr
+ * constr array
+ , constr )
+ journey_info_tac
; otherS : (unit, constr) journey_info_tac
; apP : (constr * constr list, constr) journey_info_tac
; app_reC : (constr * constr list, constr) journey_info_tac
@@ -441,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 =
@@ -474,9 +484,9 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
++ Printer.pr_leconstr_env env sigma expr_info.info
++ str " can not contain a recursive call to "
++ Id.print expr_info.f_id ) )
- | Case (ci, t, a, l) ->
+ | Case (ci, t, iv, a, l) ->
let continuation_tac_a =
- jinfo.casE (travel jinfo) (ci, t, a, l) expr_info continuation_tac
+ jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
in
travel jinfo continuation_tac_a
{expr_info with info = a; is_main_branch = false; is_final = false}
@@ -767,7 +777,8 @@ let mkDestructEq not_on_hyp expr g =
in
(g, tac, to_revert)
-let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
+let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
+ g =
let sigma = project g in
let env = pf_env g in
let f_is_present =
@@ -779,7 +790,7 @@ let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
let a' = infos.info in
let new_info =
{ infos with
- info = mkCase (ci, t, a', l)
+ info = mkCase (ci, t, iv, a', l)
; is_main_branch = expr_info.is_main_branch
; is_final = expr_info.is_final }
in
@@ -916,10 +927,10 @@ let prove_terminate = travel terminate_info
(* Equation proof *)
-let equation_case next_step (ci, a, t, l) expr_info continuation_tac infos =
+let equation_case next_step case expr_info continuation_tac infos =
observe_tac
(fun _ _ -> str "equation case")
- (terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos)
+ (terminate_case next_step case expr_info continuation_tac infos)
let rec prove_le g =
let sigma = project g in
@@ -1493,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
@@ -1652,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-03-08 06:45:28 +0000