aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml15
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/recdef.ml10
6 files changed, 23 insertions, 17 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3b95423067..8da30bd9c9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -763,12 +763,13 @@ let build_proof
end
| Cast(t,_,_) ->
build_proof do_finalize {dyn_infos with info = t} g
- | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
do_finalize dyn_infos g
| App(_,_) ->
let f,args = decompose_app sigma dyn_infos.info in
begin
match EConstr.kind sigma f with
+ | Int _ -> user_err Pp.(str "integer cannot be applied")
| App _ -> assert false (* we have collected all the app in decompose_app *)
| Proj _ -> assert false (*FIXME*)
| Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ ->
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 12b68e208c..25a7675113 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -364,7 +364,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let univs = Evd.const_univ_entry ~poly:false evd' in
+ let univs = Evd.univ_entry ~poly:false evd' in
let ce = Declare.definition_entry ~univs value in
ignore(
Declare.declare_constant
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4b6caea70d..ba0a3bbb5c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl =
construct
in
let argl =
- if List.is_empty argl
- then
- Array.to_list
- (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
- )
- else argl
+ if List.is_empty argl then
+ List.make cst_narg (mkGHole ())
+ else
+ List.make npar (mkGHole ()) @ argl
in
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
@@ -478,7 +476,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
let open CAst in
match DAst.get rt with
- | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ ->
+ | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ ->
(* do nothing (except changing type of course) *)
mk_result [] rt avoid
| GApp(_,_) ->
@@ -588,6 +586,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
+ | GInt _ -> user_err Pp.(str "Cannot apply an integer")
end (* end of the application treatement *)
| GLambda(n,_,t,b) ->
@@ -1221,7 +1220,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
TODO: Find a valid way to deal with implicit arguments here!
*)
let rec compute_cst_params relnames params gt = DAst.with_val (function
- | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
+ | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params
| GApp(f,args) ->
begin match DAst.get f with
| GVar relname' when Id.Set.mem relname' relnames ->
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5b45a8dbed..13ff19a46b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -106,6 +106,7 @@ let change_vars =
| GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported")
| GSort _ as x -> x
| GHole _ as x -> x
+ | GInt _ as x -> x
| GCast(b,c) ->
GCast(change_vars mapping b,
Glob_ops.map_cast_type (change_vars mapping) c)
@@ -285,6 +286,7 @@ let rec alpha_rt excluded rt =
)
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GSort _
+ | GInt _
| GHole _ as rt -> rt
| GCast (b,c) ->
GCast(alpha_rt excluded b,
@@ -344,6 +346,7 @@ 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 _ -> false
) x
and is_free_in_br {CAst.v=(ids,_,rt)} =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -434,6 +437,7 @@ let replace_var_by_term x_id term =
| GRec _ -> raise (UserError(None,str "Not handled GRec"))
| GSort _
| GHole _ as rt -> rt
+ | GInt _ as rt -> rt
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
Glob_ops.map_cast_type replace_var_by_pattern c)
@@ -516,7 +520,7 @@ let expand_as =
| PatCstr(_,patl,_) -> List.fold_left add_as map patl
in
let rec expand_as map = DAst.map (function
- | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt
+ | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt
| GVar id as rt ->
begin
try
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3a04c753ea..42dc66dcf4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -166,7 +166,7 @@ let build_newrecursive
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
let evd = Evd.from_env env0 in
- let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
+ let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in
let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
let open Context.Named.Declaration in
(EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
@@ -201,7 +201,7 @@ let is_rec names =
let check_id id names = Id.Set.mem id names in
let rec lookup names gt = match DAst.get gt with
| GVar(id) -> check_id id names
- | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
+ | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false
| GCast(b,_) -> lookup names b
| GRec _ -> error "GRec not handled"
| GIf(b,_,lhs,rhs) ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 38f27f760b..a8517e9ab1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -306,6 +306,7 @@ let check_not_nested sigma forbidden e =
let rec check_not_nested e =
match EConstr.kind sigma e with
| Rel _ -> ()
+ | Int _ -> ()
| Var x ->
if Id.List.mem x forbidden
then user_err ~hdr:"Recdef.check_not_nested"
@@ -487,7 +488,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
| _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".")
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
- | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
let new_continuation_tac =
jinfo.otherS () expr_info continuation_tac in
new_continuation_tac expr_info g
@@ -1294,6 +1295,7 @@ let is_opaque_constant c =
| Declarations.OpaqueDef _ -> Proof_global.Opaque
| Declarations.Undef _ -> Proof_global.Opaque
| Declarations.Def _ -> Proof_global.Transparent
+ | Declarations.Primitive _ -> Proof_global.Opaque
let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
(* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
@@ -1516,10 +1518,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let open CVars in
let env = Global.env() in
let evd = Evd.from_env env in
- let evd, function_type = interp_type_evars env evd type_of_f in
+ let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in
let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
+ let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in
let evd = Evd.minimize_universes evd in
let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in
let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
@@ -1545,7 +1547,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
+ let univs = Evd.univ_entry ~poly:false evd in
declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:08:11 +0000