aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml75
-rw-r--r--plugins/funind/functional_principles_types.ml51
-rw-r--r--plugins/funind/g_indfun.mlg20
-rw-r--r--plugins/funind/glob_term_to_relation.ml131
-rw-r--r--plugins/funind/indfun.ml11
-rw-r--r--plugins/funind/indfun_common.ml32
-rw-r--r--plugins/funind/indfun_common.mli11
-rw-r--r--plugins/funind/invfun.ml37
-rw-r--r--plugins/funind/recdef.ml103
9 files changed, 251 insertions, 220 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6fd2f7c2bc..16f376931e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -2,6 +2,7 @@ open Printer
open CErrors
open Util
open Constr
+open Context
open EConstr
open Vars
open Namegen
@@ -44,10 +45,6 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
*)
-let pr_leconstr_fp =
- let sigma, env = Pfedit.get_current_context () in
- Printer.pr_leconstr_env env sigma
-
let debug_queue = Stack.create ()
let rec print_debug_queue e =
@@ -163,7 +160,7 @@ let rec incompatible_constructor_terms sigma t1 t2 =
List.exists2 (incompatible_constructor_terms sigma) arg1 arg2
)
-let is_incompatible_eq sigma t =
+let is_incompatible_eq env sigma t =
let res =
try
match EConstr.kind sigma t with
@@ -175,7 +172,7 @@ let is_incompatible_eq sigma t =
| _ -> false
with e when CErrors.noncritical e -> false
in
- if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t);
+ if res then observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t);
res
let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -302,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
in
let old_context_length = List.length context + 1 in
let witness_fun =
- mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t,
+ mkLetIn(make_annot Anonymous Sorts.Relevant,make_refl_eq constructor t1_typ (fst t1),t,
mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
)
in
@@ -312,7 +309,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
try
let witness = Int.Map.find i sub in
if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
- (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
+ (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_annot decl,
+ witness, RelDecl.get_type decl, witness_fun))
with Not_found ->
(mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
)
@@ -428,7 +426,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
else if isProd sigma type_of_hyp
then
begin
- let (x,t_x,t') = destProd sigma type_of_hyp in
+ let (x,t_x,t') = destProd sigma type_of_hyp in
let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in
if is_property sigma ptes_infos t_x actual_real_type_of_hyp then
begin
@@ -478,7 +476,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
(* ); *)
raise TOREMOVE; (* False -> .. useless *)
end
- else if is_incompatible_eq sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *)
+ else if is_incompatible_eq env sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *)
else if eq_constr sigma t_x coq_True (* Trivial => we remove this precons *)
then
(* observe (str "In "++Ppconstr.pr_id hyp_id++ *)
@@ -541,7 +539,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
(scan_type new_context new_t')
with NoChange ->
(* Last thing todo : push the rel in the context and continue *)
- scan_type (LocalAssum (x,t_x) :: context) t'
+ scan_type (LocalAssum (x,t_x) :: context) t'
end
end
else
@@ -610,7 +608,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
anomaly (Pp.str "cannot compute new term value.")
in
let fun_body =
- mkLambda(Anonymous,
+ mkLambda(make_annot Anonymous Sorts.Relevant,
pf_unsafe_type_of g' term,
Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
)
@@ -724,7 +722,7 @@ let build_proof
(treat_new_case
ptes_infos
nb_instantiate_partial
- (build_proof do_finalize)
+ (build_proof env sigma do_finalize)
t
dyn_infos)
g'
@@ -735,8 +733,8 @@ let build_proof
]
g
in
- build_proof do_finalize_t {dyn_infos with info = t} g
- | Lambda(n,t,b) ->
+ build_proof env sigma do_finalize_t {dyn_infos with info = t} g
+ | Lambda(n,t,b) ->
begin
match EConstr.kind sigma (pf_concl g) with
| Prod _ ->
@@ -751,7 +749,7 @@ let build_proof
in
let new_infos = {dyn_infos with info = new_term} in
let do_prove new_hyps =
- build_proof do_finalize
+ build_proof env sigma do_finalize
{new_infos with
rec_hyps = new_hyps;
nb_rec_hyps = List.length new_hyps
@@ -764,7 +762,7 @@ let build_proof
do_finalize dyn_infos g
end
| Cast(t,_,_) ->
- build_proof do_finalize {dyn_infos with info = t} g
+ build_proof env sigma do_finalize {dyn_infos with info = t} g
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
do_finalize dyn_infos g
| App(_,_) ->
@@ -780,7 +778,7 @@ let build_proof
info = (f,args)
}
in
- build_proof_args do_finalize new_infos g
+ build_proof_args env sigma do_finalize new_infos g
| Const (c,_) when not (List.mem_f Constant.equal c fnames) ->
let new_infos =
{ dyn_infos with
@@ -788,13 +786,13 @@ let build_proof
}
in
(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
- build_proof_args do_finalize new_infos g
+ build_proof_args env sigma do_finalize new_infos g
| Const _ ->
do_finalize dyn_infos g
| Lambda _ ->
let new_term =
Reductionops.nf_beta env sigma dyn_infos.info in
- build_proof do_finalize {dyn_infos with info = new_term}
+ build_proof env sigma do_finalize {dyn_infos with info = new_term}
g
| LetIn _ ->
let new_infos =
@@ -807,11 +805,11 @@ let build_proof
h_reduce_with_zeta (Locusops.onHyp hyp_id))
dyn_infos.rec_hyps;
h_reduce_with_zeta Locusops.onConcl;
- build_proof do_finalize new_infos
+ build_proof env sigma do_finalize new_infos
]
g
| Cast(b,_,_) ->
- build_proof do_finalize {dyn_infos with info = b } g
+ build_proof env sigma do_finalize {dyn_infos with info = b } g
| Case _ | Fix _ | CoFix _ ->
let new_finalize dyn_infos =
let new_infos =
@@ -819,9 +817,9 @@ let build_proof
info = dyn_infos.info,args
}
in
- build_proof_args do_finalize new_infos
+ build_proof_args env sigma do_finalize new_infos
in
- build_proof new_finalize {dyn_infos with info = f } g
+ build_proof env sigma new_finalize {dyn_infos with info = f } g
end
| Fix _ | CoFix _ ->
user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
@@ -841,13 +839,13 @@ let build_proof
(fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
dyn_infos.rec_hyps;
h_reduce_with_zeta Locusops.onConcl;
- build_proof do_finalize new_infos
+ build_proof env sigma do_finalize new_infos
] g
| Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
- and build_proof do_finalize dyn_infos g =
+ and build_proof env sigma do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
- observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
- and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic =
+ observe_tac_stream (str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+ and build_proof_args env sigma do_finalize dyn_infos (* f_args' args *) :tactic =
fun g ->
let (f_args',args) = dyn_infos.info in
let tac : tactic =
@@ -863,12 +861,12 @@ let build_proof
let do_finalize dyn_infos =
let new_arg = dyn_infos.info in
(* tclTRYD *)
- (build_proof_args
+ (build_proof_args env sigma
do_finalize
{dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
)
in
- build_proof do_finalize
+ build_proof env sigma do_finalize
{dyn_infos with info = arg }
g
in
@@ -880,7 +878,10 @@ let build_proof
finish_proof dyn_infos)
in
(* observe_tac "build_proof" *)
- (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos)
+ fun g ->
+ let env = pf_env g in
+ let sigma = project g in
+ build_proof env sigma (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g
@@ -1149,7 +1150,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let fix_offset = List.length princ_params in
let ptes_to_fix,infos =
match EConstr.kind (project g) fbody_with_full_params with
- | Fix((idxs,i),(names,typess,bodies)) ->
+ | Fix((idxs,i),(names,typess,bodies)) ->
let bodies_with_all_params =
Array.map
(fun body ->
@@ -1164,7 +1165,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(fun i types ->
let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
{ idx = idxs.(i) - fix_offset;
- name = Nameops.Name.get_id (fresh_id names.(i));
+ name = Nameops.Name.get_id (fresh_id names.(i).binder_name);
types = types;
offset = fix_offset;
nb_realargs =
@@ -1195,9 +1196,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
applist(body,List.rev_map var_of_decl full_params))
in
match EConstr.kind (project g) body_with_full_params with
- | Fix((_,num),(_,_,bs)) ->
+ | Fix((_,num),(_,_,bs)) ->
Reductionops.nf_betaiota (pf_env g) (project g)
- (
+ (
(applist
(substl
(List.rev
@@ -1514,7 +1515,7 @@ let is_valid_hypothesis sigma predicates_name =
let rec is_valid_hypothesis typ =
is_pte typ ||
match EConstr.kind sigma typ with
- | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
+ | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
| _ -> false
in
is_valid_hypothesis
@@ -1565,7 +1566,7 @@ let prove_principle_for_gen
in
let rec_arg_id =
match List.rev post_rec_arg with
- | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id
+ | (LocalAssum ({binder_name=Name id},_) | LocalDef ({binder_name=Name id},_,_)) :: _ -> id
| _ -> assert false
in
(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index ca09cad1f3..1217ba0eba 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -14,6 +14,7 @@ open Term
open Sorts
open Util
open Constr
+open Context
open Vars
open Namegen
open Names
@@ -72,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
then List.tl args
else args
in
- Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl),
+ Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl),
Term.compose_prod real_args (mkSort new_sort))
in
let new_predicates =
@@ -137,14 +138,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| Rel n ->
begin
try match Environ.lookup_rel n env with
- | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved
+ | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved
| _ -> pre_princ,[]
with Not_found -> assert false
end
- | Prod(x,t,b) ->
- compute_new_princ_type_for_binder remove mkProd env x t b
- | Lambda(x,t,b) ->
- compute_new_princ_type_for_binder remove mkLambda env x t b
+ | Prod(x,t,b) ->
+ compute_new_princ_type_for_binder remove mkProd env x t b
+ | Lambda(x,t,b) ->
+ compute_new_princ_type_for_binder remove mkLambda env x t b
| Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
| App(f,args) when is_dom f ->
let var_to_be_removed = destRel (Array.last args) in
@@ -164,8 +165,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
applistc new_f new_args,
list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove
- | LetIn(x,v,t,b) ->
- compute_new_princ_type_for_letin remove env x v t b
+ | LetIn(x,v,t,b) ->
+ compute_new_princ_type_for_letin remove env x v t b
| _ -> pre_princ,[]
in
(* let _ = match Constr.kind pre_princ with *)
@@ -181,14 +182,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
begin
try
let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
- let new_x : Name.t = get_name (Termops.ids_of_context env) x in
- let new_env = Environ.push_rel (LocalAssum (x,t)) env in
+ let new_x = map_annot (get_name (Termops.ids_of_context env)) x in
+ let new_env = Environ.push_rel (LocalAssum (x,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
else
(
- bind_fun(new_x,new_t,new_b),
+ bind_fun(new_x,new_t,new_b),
list_union_eq
Constr.equal
binders_to_remove_from_t
@@ -210,14 +211,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
try
let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
- let new_x : Name.t = get_name (Termops.ids_of_context env) x in
- let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
+ let new_x = map_annot (get_name (Termops.ids_of_context env)) x in
+ let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
else
(
- mkLetIn(new_x,new_v,new_t,new_b),
+ mkLetIn(new_x,new_v,new_t,new_b),
list_union_eq
Constr.equal
(list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v)
@@ -250,8 +251,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
it_mkProd_or_LetIn
(it_mkProd_or_LetIn
- pre_res (List.map (function Context.Named.Declaration.LocalAssum (id,b) -> LocalAssum (Name (Hashtbl.find tbl id), b)
- | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b))
+ pre_res (List.map (function
+ | Context.Named.Declaration.LocalAssum (id,b) ->
+ LocalAssum (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, b)
+ | Context.Named.Declaration.LocalDef (id,t,b) ->
+ LocalDef (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, t, b))
new_predicates)
)
(List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params)
@@ -264,7 +268,7 @@ let change_property_sort evd toSort princ princName =
let princ_info = compute_elim_sig evd princ in
let change_sort_in_predicate decl =
LocalAssum
- (get_name decl,
+ (get_annot decl,
let args,ty = decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in
let s = destSort ty in
Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
@@ -414,7 +418,7 @@ let get_funs_constant mp =
| Fix((_,(na,_,_))) ->
Array.mapi
(fun i na ->
- match na with
+ match na.binder_name with
| Name id ->
let const = Constant.make2 mp (Label.of_id id) in
const,i
@@ -451,7 +455,8 @@ let get_funs_constant mp =
let first_params = List.hd l_params in
List.iter
(fun params ->
- if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
+ if not (List.equal (fun (n1, c1) (n2, c2) ->
+ eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
then user_err Pp.(str "Not a mutal recursive block")
)
l_params
@@ -461,7 +466,7 @@ let get_funs_constant mp =
try
let extract_info is_first body =
match Constr.kind body with
- | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
+ | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
| _ ->
if is_first && Int.equal (List.length l_bodies) 1
then raise Not_Rec
@@ -469,9 +474,9 @@ let get_funs_constant mp =
in
let first_infos = extract_info true (List.hd l_bodies) in
let check body = (* Hope this is correct *)
- let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
- Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
- Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
+ let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
+ Array.equal Int.equal ia1 ia2 && Array.equal (eq_annot Name.equal) na1 na2 &&
+ Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
in
if not (eq_infos first_infos (extract_info false body))
then user_err Pp.(str "Not a mutal recursive block")
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index c4f8843e51..6f67ab4d8b 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -29,10 +29,10 @@ DECLARE PLUGIN "recdef_plugin"
{
-let pr_fun_ind_using prc prlc _ opt_c =
+let pr_fun_ind_using env sigma prc prlc _ opt_c =
match opt_c with
| None -> mt ()
- | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
+ | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env sigma) (prlc env sigma) b)
(* Duplication of printing functions because "'a with_bindings" is
(internally) not uniform in 'a: indeed constr_with_bindings at the
@@ -47,15 +47,15 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
let env = Global.env () in
let evd = Evd.from_env env in
let (_, b) = b env evd in
- spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
+ spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env evd) (prlc env evd) b)
}
ARGUMENT EXTEND fun_ind_using
TYPED AS constr_with_bindings option
PRINTED BY { pr_fun_ind_using_typed }
- RAW_PRINTED BY { pr_fun_ind_using }
- GLOB_PRINTED BY { pr_fun_ind_using }
+ RAW_PRINTED BY { pr_fun_ind_using env sigma }
+ GLOB_PRINTED BY { pr_fun_ind_using env sigma }
| [ "using" constr_with_bindings(c) ] -> { Some c }
| [ ] -> { None }
END
@@ -119,26 +119,26 @@ END
{
-let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc
+let pr_constr_comma_sequence env sigma prc _ _ = prlist_with_sep pr_comma (prc env sigma)
}
ARGUMENT EXTEND constr_comma_sequence'
TYPED AS constr list
- PRINTED BY { pr_constr_comma_sequence }
+ PRINTED BY { pr_constr_comma_sequence env sigma }
| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l }
| [ constr(c) ] -> { [c] }
END
{
-let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+let pr_auto_using env sigma prc _prlc _prt = Pptactic.pr_auto_using (prc env sigma)
}
ARGUMENT EXTEND auto_using'
TYPED AS constr list
- PRINTED BY { pr_auto_using }
+ PRINTED BY { pr_auto_using env sigma }
| [ "using" constr_comma_sequence'(l) ] -> { l }
| [ ] -> { [] }
END
@@ -170,7 +170,7 @@ END
{
let () =
- let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
+ let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
}
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index ba0a3bbb5c..f4807954a7 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -2,6 +2,7 @@ open Printer
open Pp
open Names
open Constr
+open Context
open Vars
open Glob_term
open Glob_ops
@@ -343,20 +344,21 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
+ let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
+ let na = make_annot id Sorts.Relevant in (* TODO relevance *)
(match raw_value with
| None ->
- EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env
+ EConstr.push_named (NamedDecl.LocalAssum (na,typ)) env
| Some value ->
- EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env)
+ EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env)
-let add_pat_variables pat typ env : Environ.env =
+let add_pat_variables sigma pat typ env : Environ.env =
let rec add_pat_variables env pat typ : Environ.env =
observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
match DAst.get pat with
- | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
+ | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (make_annot na Sorts.Relevant,typ)) env
| PatCstr(c,patl,na) ->
let Inductiveops.IndType(indf,indargs) =
try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
@@ -373,18 +375,19 @@ let add_pat_variables pat typ env : Environ.env =
Context.Rel.fold_outside
(fun decl (env,ctxt) ->
let open Context.Rel.Declaration in
- let sigma, _ = Pfedit.get_current_context () in
match decl with
- | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
- | LocalAssum (Name id, t) ->
+ | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false
+ | LocalAssum ({binder_name=Name id} as na, t) ->
+ let na = {na with binder_name=id} in
let new_t = substl ctxt t in
observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl ()
);
let open Context.Named.Declaration in
- (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
- | LocalDef (Name id, v, t) ->
+ (Environ.push_named (LocalAssum (na,new_t)) env,mkVar id::ctxt)
+ | LocalDef ({binder_name=Name id} as na, v, t) ->
+ let na = {na with binder_name=id} in
let new_t = substl ctxt t in
let new_v = substl ctxt v in
observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
@@ -394,7 +397,7 @@ let add_pat_variables pat typ env : Environ.env =
str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl ()
);
let open Context.Named.Declaration in
- (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
+ (Environ.push_named (LocalDef (na,new_v,new_t)) env,mkVar id::ctxt)
)
(Environ.rel_context new_env)
~init:(env,[])
@@ -472,7 +475,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function
*)
-let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
+let rec build_entry_lc env sigma 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
@@ -484,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let args_res : (glob_constr list) build_entry_return =
List.fold_right (* create the arguments lists of constructors and combine them *)
(fun arg ctxt_argsl ->
- let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
+ let arg_res = build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg in
combine_results combine_args arg_res ctxt_argsl
)
args
@@ -503,7 +506,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| _ ->
GApp(t,l)
in
- build_entry_lc env funnames avoid (aux f args)
+ build_entry_lc env sigma funnames avoid (aux f args)
| GVar id when Id.Set.mem id funnames ->
(* if we have [f t1 ... tn] with [f]$\in$[fnames]
then we create a fresh variable [res],
@@ -567,7 +570,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
in
build_entry_lc
env
- funnames
+ sigma
+ funnames
avoid
(mkGLetIn(new_n,v,t,mkGApp(new_b,args)))
| GCases _ | GIf _ | GLetTuple _ ->
@@ -575,7 +579,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
we first compute the result from the case and
then combine each of them with each of args one
*)
- let f_res = build_entry_lc env funnames args_res.to_avoid f in
+ let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
| GCast(b,_) ->
(* for an applied cast we just trash the cast part
@@ -583,7 +587,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
WARNING: We need to restart since [b] itself should be an application term
*)
- build_entry_lc env funnames avoid (mkGApp(b,args))
+ build_entry_lc env sigma 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")
@@ -595,14 +599,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
then the one corresponding to the type
and combine the two result
*)
- let t_res = build_entry_lc env funnames avoid t in
+ let t_res = build_entry_lc env sigma funnames avoid t in
let new_n =
match n with
| Name _ -> n
| Anonymous -> Name (Indfun_common.fresh_id [] "_x")
in
let new_env = raw_push_named (new_n,None,t) env in
- let b_res = build_entry_lc new_env funnames avoid b in
+ let b_res = build_entry_lc new_env sigma funnames avoid b in
combine_results (combine_lam new_n) t_res b_res
| GProd(n,_,t,b) ->
(* we first compute the list of constructor
@@ -610,9 +614,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
then the one corresponding to the type
and combine the two result
*)
- let t_res = build_entry_lc env funnames avoid t in
+ let t_res = build_entry_lc env sigma funnames avoid t in
let new_env = raw_push_named (n,None,t) env in
- let b_res = build_entry_lc new_env funnames avoid b in
+ let b_res = build_entry_lc new_env sigma funnames avoid b in
if List.length t_res.result = 1 && List.length b_res.result = 1
then combine_results (combine_prod2 n) t_res b_res
else combine_results (combine_prod n) t_res b_res
@@ -623,22 +627,23 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
and combine the two result
*)
let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
- let v_res = build_entry_lc env funnames avoid v in
+ let v_res = build_entry_lc env sigma funnames avoid v in
let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
+ let v_r = Sorts.Relevant in (* TODO relevance *)
let new_env =
match n with
Anonymous -> env
- | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
- in
- let b_res = build_entry_lc new_env funnames avoid b in
+ | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,v_as_constr,v_type)) env
+ in
+ let b_res = build_entry_lc new_env sigma funnames avoid b in
combine_results (combine_letin n) v_res b_res
| GCases(_,_,el,brl) ->
(* we create the discrimination function
and treat the case itself
*)
let make_discr = make_discr_match brl in
- build_entry_lc_from_case env funnames make_discr el brl avoid
+ build_entry_lc_from_case env sigma funnames make_discr el brl avoid
| GIf(b,(na,e_option),lhs,rhs) ->
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
@@ -661,7 +666,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
mkGCases(None,[(b,(Anonymous,None))],brl)
in
(* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
- build_entry_lc env funnames avoid match_expr
+ build_entry_lc env sigma funnames avoid match_expr
| GLetTuple(nal,_,b,e) ->
begin
let nal_as_glob_constr =
@@ -685,13 +690,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
assert (Int.equal (Array.length case_pats) 1);
let br = CAst.make ([],[case_pats.(0)],e) in
let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
- build_entry_lc env funnames avoid match_expr
+ build_entry_lc env sigma funnames avoid match_expr
end
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,_) ->
- build_entry_lc env funnames avoid b
-and build_entry_lc_from_case env funname make_discr
+ build_entry_lc env sigma funnames avoid b
+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 =
@@ -709,7 +714,7 @@ and build_entry_lc_from_case env funname make_discr
let case_resl =
List.fold_right
(fun (case_arg,_) ctxt_argsl ->
- let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in
+ let arg_res = build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg in
combine_results combine_args arg_res ctxt_argsl
)
el
@@ -726,7 +731,7 @@ and build_entry_lc_from_case env funname make_discr
List.map
(fun ca ->
let res = build_entry_lc_from_case_term
- env types
+ env sigma types
funname (make_discr)
[] brl
case_resl.to_avoid
@@ -743,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr
[] results
}
-and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
+and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to_prevent brl avoid
matched_expr =
match brl with
| [] -> (* computed_branches *) {result = [];to_avoid = avoid}
@@ -754,14 +759,14 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
(* building a list of precondition stating that we are not in this branch
(will be used in the following recursive calls)
*)
- let new_env = List.fold_right2 add_pat_variables patl types env in
+ let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in
let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
List.map2
(fun pat typ ->
fun avoid pat'_as_term ->
let renamed_pat,_,_ = alpha_pat avoid pat in
let pat_ids = get_pattern_id renamed_pat in
- let env_with_pat_ids = add_pat_variables pat typ new_env in
+ let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
List.fold_right
(fun id acc ->
let typ_of_id =
@@ -793,6 +798,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
let brl'_res =
build_entry_lc_from_case_term
env
+ sigma
types
funname
make_discr
@@ -857,7 +863,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
)
in
(* We compute the result of the value returned by the branch*)
- let return_res = build_entry_lc new_env funname new_avoid return in
+ let return_res = build_entry_lc new_env sigma funname new_avoid return in
(* and combine it with the preconds computed for this branch *)
let this_branch_res =
List.map
@@ -890,8 +896,7 @@ let same_raw_term rt1 rt2 =
| GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2
| GHole _, GHole _ -> true
| _ -> false
-let decompose_raw_eq lhs rhs =
- let _, env = Pfedit.get_current_context () in
+let decompose_raw_eq env lhs rhs =
let rec decompose_raw_eq lhs rhs acc =
observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs);
let (rhd,lrhs) = glob_decompose_app rhs in
@@ -939,9 +944,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let new_t =
mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
in
- let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
- let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
- let new_b,id_to_exclude =
+ let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
+ let r = Sorts.Relevant in (* TODO relevance *)
+ let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+ let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
args new_crossed_types
@@ -974,9 +980,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let new_args = List.map (replace_var_by_term id rt) args in
let subst_b =
if is_in_b then b else replace_var_by_term id rt b
- in
- let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
- let new_b,id_to_exclude =
+ in
+ let r = Sorts.Relevant in (* TODO relevance *)
+ let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+ let new_b,id_to_exclude =
rebuild_cons
new_env
nb_args relname
@@ -1057,8 +1064,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
in
let new_env =
let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
- EConstr.push_rel (LocalAssum (n,t')) env
- in
+ let r = Sorts.Relevant in (* TODO relevance *)
+ EConstr.push_rel (LocalAssum (make_annot n r,t')) env
+ in
let new_b,id_to_exclude =
rebuild_cons
new_env
@@ -1078,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
->
begin
try
- let l = decompose_raw_eq rt1 rt2 in
+ let l = decompose_raw_eq env rt1 rt2 in
if List.length l > 1
then
let new_rt =
@@ -1095,8 +1103,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
with Continue ->
observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
- let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
- let new_b,id_to_exclude =
+ let r = Sorts.Relevant in (* TODO relevance *)
+ let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+ let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
args new_crossed_types
@@ -1111,8 +1120,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ ->
observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
- let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
- let new_b,id_to_exclude =
+ let r = Sorts.Relevant in (* TODO relevance *)
+ let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+ let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
args new_crossed_types
@@ -1132,8 +1142,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
match n with
| Name id ->
- let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
- let new_b,id_to_exclude =
+ let r = Sorts.Relevant in (* TODO relevance *)
+ let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+ let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
(args@[mkGVar id])new_crossed_types
@@ -1158,7 +1169,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let type_t' = Typing.unsafe_type_of env evd t' in
let t' = EConstr.Unsafe.to_constr t' in
let type_t' = EConstr.Unsafe.to_constr type_t' in
- let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
+ let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1182,8 +1193,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
depth t
in
let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
- let new_env = EConstr.push_rel (LocalAssum (na,t')) env in
- let new_b,id_to_exclude =
+ let r = Sorts.Relevant in (* TODO relevance *)
+ let new_env = EConstr.push_rel (LocalAssum (make_annot na r,t')) env in
+ let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
args (t::crossed_types)
@@ -1320,7 +1332,7 @@ let do_build_inductive
let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
let t = EConstr.Unsafe.to_constr t in
evd,
- Environ.push_named (LocalAssum (id,t))
+ Environ.push_named (LocalAssum (make_annot id Sorts.Relevant,t))
env
)
funnames
@@ -1334,7 +1346,7 @@ let do_build_inductive
resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt
) rta
in
- let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
+ let resa = Array.map (build_entry_lc env evd funnames_as_set []) rta in
let env_with_graphs =
let rel_arity i funargs = (* Rebuilding arities (with parameters) *)
let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list =
@@ -1364,7 +1376,8 @@ let do_build_inductive
Util.Array.fold_left2 (fun env rel_name rel_ar ->
let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in
let rex = EConstr.Unsafe.to_constr rex in
- Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities
+ let r = Sorts.Relevant in (* TODO relevance *)
+ Environ.push_named (LocalAssum (make_annot rel_name r,rex)) env) env relnames rel_arities
in
(* and of the real constructors*)
let constr i res =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 42dc66dcf4..b69ca7080c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -3,6 +3,7 @@ open Sorts
open Util
open Names
open Constr
+open Context
open EConstr
open Pp
open Indfun_common
@@ -49,7 +50,8 @@ let functional_induction with_clean c princl pat =
user_err (str "Cannot find induction information on "++
Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
- match Tacticals.elimination_sort_of_goal g with
+ match Tacticals.elimination_sort_of_goal g with
+ | InSProp -> finfo.sprop_lemma
| InProp -> finfo.prop_lemma
| InSet -> finfo.rec_lemma
| InType -> finfo.rect_lemma
@@ -169,7 +171,8 @@ let build_newrecursive
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))
+ let r = Sorts.Relevant in (* TODO relevance *)
+ (EConstr.push_named (LocalAssum (make_annot recname r,arity)) env, Id.Map.add recname impl impls))
(env0,Constrintern.empty_internalization_env) lnameargsardef in
let recdef =
(* Declare local notations *)
@@ -621,8 +624,8 @@ let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
- let constr_expr_typel =
+ let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
+ let constr_expr_typel =
with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index cba3cc3d42..e34323abf4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -199,6 +199,7 @@ type function_info =
rect_lemma : Constant.t option;
rec_lemma : Constant.t option;
prop_lemma : Constant.t option;
+ sprop_lemma : Constant.t option;
is_general : bool; (* Has this function been defined using general recursive definition *)
}
@@ -249,6 +250,7 @@ let subst_Function (subst,finfos) =
let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in
+ let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
equation_lemma' == finfos.equation_lemma &&
@@ -256,7 +258,8 @@ let subst_Function (subst,finfos) =
completeness_lemma' == finfos.completeness_lemma &&
rect_lemma' == finfos.rect_lemma &&
rec_lemma' == finfos.rec_lemma &&
- prop_lemma' == finfos.prop_lemma
+ prop_lemma' == finfos.prop_lemma &&
+ sprop_lemma' == finfos.sprop_lemma
then finfos
else
{ function_constant = function_constant';
@@ -267,17 +270,16 @@ let subst_Function (subst,finfos) =
rect_lemma = rect_lemma' ;
rec_lemma = rec_lemma';
prop_lemma = prop_lemma';
+ sprop_lemma = sprop_lemma';
is_general = finfos.is_general
}
let discharge_Function (_,finfos) = Some finfos
-let pr_ocst c =
- let sigma, env = Pfedit.get_current_context () in
+let pr_ocst env sigma c =
Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
-let pr_info f_info =
- let sigma, env = Pfedit.get_current_context () in
+let pr_info env sigma f_info =
str "function_constant := " ++
Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
str "function_constant_type := " ++
@@ -285,17 +287,17 @@ let pr_info f_info =
Printer.pr_lconstr_env env sigma
(fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
- str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
- str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
- str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++
- str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
- str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
- str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
+ str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++
+ str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++
+ str "correctness_lemma := " ++ pr_ocst env sigma f_info.correctness_lemma ++ fnl () ++
+ str "rect_lemma := " ++ pr_ocst env sigma f_info.rect_lemma ++ fnl () ++
+ str "rec_lemma := " ++ pr_ocst env sigma f_info.rec_lemma ++ fnl () ++
+ str "prop_lemma := " ++ pr_ocst env sigma f_info.prop_lemma ++ fnl () ++
str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
-let pr_table tb =
+let pr_table env sigma tb =
let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
- Pp.prlist_with_sep fnl pr_info l
+ Pp.prlist_with_sep fnl (pr_info env sigma) l
let in_Function : function_info -> Libobject.obj =
let open Libobject in
@@ -333,6 +335,7 @@ let add_Function is_general f =
and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
+ and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind")
and graph_ind =
match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
@@ -345,6 +348,7 @@ let add_Function is_general f =
rect_lemma = rect_lemma;
rec_lemma = rec_lemma;
prop_lemma = prop_lemma;
+ sprop_lemma = sprop_lemma;
graph_ind = graph_ind;
is_general = is_general
@@ -352,7 +356,7 @@ let add_Function is_general f =
in
update_Function finfos
-let pr_table () = pr_table !from_function
+let pr_table env sigma = pr_table env sigma !from_function
(*********************************)
(* Debuging *)
let functional_induction_rewrite_dependent_proofs = ref true
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1e0b95df34..12facc5744 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -70,6 +70,7 @@ type function_info =
rect_lemma : Constant.t option;
rec_lemma : Constant.t option;
prop_lemma : Constant.t option;
+ sprop_lemma : Constant.t option;
is_general : bool;
}
@@ -82,8 +83,8 @@ val update_Function : function_info -> unit
(** debugging *)
-val pr_info : function_info -> Pp.t
-val pr_table : unit -> Pp.t
+val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t
+val pr_table : Environ.env -> Evd.evar_map -> Pp.t
(* val function_debug : bool ref *)
@@ -109,9 +110,9 @@ val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_referenc
val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
- (Names.Name.t * EConstr.t) list * EConstr.t
-val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
-val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+ (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
+val compose_lam : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
+val compose_prod : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
type tcc_lemma_value =
| Undefined
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 95e2e9f6e5..37dbfec4c9 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -15,6 +15,7 @@ open Util
open Names
open Term
open Constr
+open Context
open EConstr
open Vars
open Pp
@@ -142,12 +143,13 @@ let generate_type evd g_to_f f graph i =
\[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \]
i*)
let pre_ctxt =
- LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
+ LocalAssum (make_annot (Name res_id) Sorts.Relevant, lift 1 res_type) ::
+ LocalDef (make_annot (Name fv_id) Sorts.Relevant, mkApp (f,args_as_rels), res_type) :: fun_ctxt
in
(*i and we can return the solution depending on which lemma type we are defining i*)
if g_to_f
- then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
- else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+ then LocalAssum (make_annot Anonymous Sorts.Relevant,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+ else LocalAssum (make_annot Anonymous Sorts.Relevant,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
(*
@@ -270,10 +272,10 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
let sigma = project g in
match EConstr.kind sigma type_of_hid with
- | Prod(_,_,t') ->
+ | Prod(_,_,t') ->
begin
match EConstr.kind sigma t' with
- | Prod(_,t'',t''') ->
+ | Prod(_,t'',t''') ->
begin
match EConstr.kind sigma t'',EConstr.kind sigma t''' with
| App(eq,args), App(graph',_)
@@ -358,17 +360,16 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
(* end of branche proof *)
let lemmas =
Array.map
- (fun ((_,(ctxt,concl))) ->
- match ctxt with
- | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.")
- | hres::res::decl::ctxt ->
- let res = EConstr.it_mkLambda_or_LetIn
- (EConstr.it_mkProd_or_LetIn concl [hres;res])
- (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
- in
- res
- )
- lemmas_types_infos
+ (fun ((_,(ctxt,concl))) ->
+ match ctxt with
+ | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.")
+ | hres::res::decl::ctxt ->
+ let res = EConstr.it_mkLambda_or_LetIn
+ (EConstr.it_mkProd_or_LetIn concl [hres;res])
+ (LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl) :: ctxt)
+ in
+ res)
+ lemmas_types_infos
in
let param_names = fst (List.chop princ_infos.nparams args_names) in
let params = List.map mkVar param_names in
@@ -429,7 +430,7 @@ let generalize_dependent_of x hyp g =
let open Context.Named.Declaration in
tclMAP
(function
- | LocalAssum (id,t) when not (Id.equal id hyp) &&
+ | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) &&
(Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
| _ -> tclIDTAC
)
@@ -456,7 +457,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
let eq_ind = make_eq () in
let sigma = project g in
match EConstr.kind sigma (pf_concl g) with
- | Prod(_,t,t') ->
+ | Prod(_,t,t') ->
begin
match EConstr.kind sigma t with
| App(eq,args) when (EConstr.eq_constr sigma eq eq_ind) ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8746c37309..e19741a4e9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -12,6 +12,7 @@
module CVars = Vars
open Constr
+open Context
open EConstr
open Vars
open Namegen
@@ -57,10 +58,6 @@ let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global
let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
let arith_Lt = ["Coq"; "Arith";"Lt"]
-let pr_leconstr_rd =
- let sigma, env = Pfedit.get_current_context () in
- Printer.pr_leconstr_env env sigma
-
let coq_init_constant s =
EConstr.of_constr (
UnivGen.constr_of_monomorphic_global @@
@@ -182,7 +179,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
)
in
let context = List.map
- (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al))
+ (fun (x, c) -> LocalAssum (make_annot (Name x) Sorts.Relevant, c)) (List.combine rev_x_id_l (List.rev al))
in
let env = Environ.push_rel_context context (Global.env ()) in
let glob_body =
@@ -302,7 +299,7 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
(* [check_not_nested forbidden e] checks that [e] does not contains any variable
of [forbidden]
*)
-let check_not_nested sigma forbidden e =
+let check_not_nested env sigma forbidden e =
let rec check_not_nested e =
match EConstr.kind sigma e with
| Rel _ -> ()
@@ -329,7 +326,6 @@ let check_not_nested sigma forbidden e =
try
check_not_nested e
with UserError(_,p) ->
- let _, env = Pfedit.get_current_context () in
user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p)
(* ['a info] contains the local information for traveling *)
@@ -388,9 +384,9 @@ let add_vars sigma forbidden e =
let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
fun g ->
let rev_context,b = decompose_lam_n (project g) nb_lam e in
- let ids = List.fold_left (fun acc (na,_) ->
+ let ids = List.fold_left (fun acc (na,_) ->
let pre_id =
- match na with
+ match na.binder_name with
| Name x -> x
| Anonymous -> ano_id
in
@@ -433,10 +429,10 @@ 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")
| Proj _ -> user_err Pp.(str "Function cannot treat projections")
- | LetIn(na,b,t,e) ->
+ | LetIn(na,b,t,e) ->
begin
let new_continuation_tac =
- jinfo.letiN (na,b,t,e) expr_info continuation_tac
+ jinfo.letiN (na.binder_name,b,t,e) expr_info continuation_tac
in
travel jinfo new_continuation_tac
{expr_info with info = b; is_final=false} g
@@ -445,15 +441,15 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
| Prod _ ->
begin
try
- check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+ check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
- | Lambda(n,t,b) ->
+ | Lambda(n,t,b) ->
begin
try
- check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+ check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
@@ -506,10 +502,11 @@ and travel_args jinfo is_final continuation_tac infos =
in
travel jinfo new_continuation_tac
{infos with info=arg;is_final=false}
-and travel jinfo continuation_tac expr_info =
- observe_tac
- (str jinfo.message ++ pr_leconstr_rd expr_info.info)
- (travel_aux jinfo continuation_tac expr_info)
+and travel jinfo continuation_tac expr_info =
+ fun g ->
+ observe_tac
+ (str jinfo.message ++ Printer.pr_leconstr_env (pf_env g) (project g) expr_info.info)
+ (travel_aux jinfo continuation_tac expr_info) g
(* Termination proof *)
@@ -651,7 +648,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info g =
let new_forbidden =
let forbid =
try
- check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) b;
+ check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) b;
true
with e when CErrors.noncritical e -> false
in
@@ -710,7 +707,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
let sigma = project g in
let f_is_present =
try
- check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) a;
+ check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) a;
false
with e when CErrors.noncritical e ->
true
@@ -739,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
let terminate_app_rec (f,args) expr_info continuation_tac _ g =
let sigma = project g in
- List.iter (check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids))
+ List.iter (check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids))
args;
begin
try
@@ -853,8 +850,8 @@ let rec prove_le g =
EConstr.is_global sigma (le ()) c
| _ -> false
in
- let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
- in
+ let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in
+ let h = h.binder_name in
let y =
let _,args = decompose_app sigma t in
List.hd (List.tl args)
@@ -877,10 +874,10 @@ let rec make_rewrite_list expr_info max = function
let sigma = project g in
let t_eq = compute_renamed_type g (mkVar hp) in
let k,def =
- let k_na,_,t = destProd sigma t_eq in
- let _,_,t = destProd sigma t in
- let def_na,_,_ = destProd sigma t in
- Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
+ let k_na,_,t = destProd sigma t_eq in
+ let _,_,t = destProd sigma t in
+ let def_na,_,_ = destProd sigma t in
+ Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name
in
Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
@@ -903,10 +900,10 @@ let make_rewrite expr_info l hp max =
let sigma = project g in
let t_eq = compute_renamed_type g (mkVar hp) in
let k,def =
- let k_na,_,t = destProd sigma t_eq in
- let _,_,t = destProd sigma t in
- let def_na,_,_ = destProd sigma t in
- Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
+ let k_na,_,t = destProd sigma t_eq in
+ let _,_,t = destProd sigma t in
+ let def_na,_,_ = destProd sigma t in
+ Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name
in
observe_tac (str "general_rewrite_bindings")
(Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
@@ -986,13 +983,19 @@ let rec intros_values_eq expr_info acc =
))
let equation_others _ expr_info continuation_tac infos =
+ fun g ->
+ let env = pf_env g in
+ let sigma = project g in
if expr_info.is_final && expr_info.is_main_branch
- then
- observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info)
+ then
+ observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info)
(tclTHEN
(continuation_tac infos)
- (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info [])))
- else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos)
+ (fun g ->
+ let env = pf_env g in
+ let sigma = project g in
+ observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []) g)) g
+ else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) g
let equation_app f_and_args expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
@@ -1054,20 +1057,19 @@ let compute_terminate_type nb_args func =
let right = mkRel 5 in
let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in
let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in
- let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in
+ let result = (mkProd (make_annot (Name def_id) Sorts.Relevant, lift 4 a_arrow_b, equality)) in
let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in
let nb_iter =
mkApp(delayed_force ex,
[|delayed_force nat;
(mkLambda
- (Name
- p_id,
+ (make_annot (Name p_id) Sorts.Relevant,
delayed_force nat,
- (mkProd (Name k_id, delayed_force nat,
- mkArrow cond result))))|])in
+ (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat,
+ mkArrow cond Sorts.Relevant result))))|])in
let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref),
[|b;
- (mkLambda (Name v_id, b, nb_iter))|]) in
+ (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in
compose_prod rev_args value
@@ -1165,15 +1167,15 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let func_body = EConstr.of_constr func_body in
let (f_name, _, body1) = destLambda sigma func_body in
let f_id =
- match f_name with
+ match f_name.binder_name with
| Name f_id -> next_ident_away_in_goal f_id ids
| Anonymous -> anomaly (Pp.str "Anonymous function.")
in
let n_names_types,_ = decompose_lam_n sigma nb_args body1 in
let n_ids,ids =
List.fold_left
- (fun (n_ids,ids) (n_name,_) ->
- match n_name with
+ (fun (n_ids,ids) (n_name,_) ->
+ match n_name.binder_name with
| Name id ->
let n_id = next_ident_away_in_goal id ids in
n_id::n_ids,n_id::ids
@@ -1270,12 +1272,12 @@ let is_rec_res id =
let clear_goals sigma =
let rec clear_goal t =
match EConstr.kind sigma t with
- | Prod(Name id as na,t',b) ->
+ | Prod({binder_name=Name id} as na,t',b) ->
let b' = clear_goal b in
if noccurn sigma 1 b' && (is_rec_res id)
then Vars.lift (-1) b'
else if b' == b then t
- else mkProd(na,t',b')
+ else mkProd(na,t',b')
| _ -> EConstr.map sigma clear_goal t
in
List.map clear_goal
@@ -1417,7 +1419,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
- let evd, env = Pfedit.get_current_context () in
+ let evd, env = Pfedit.get_current_context () in (* XXX *)
Lemmas.start_proof thm_name
(Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook;
@@ -1469,7 +1471,7 @@ let (com_eqn : int -> Id.t ->
| ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
- let evd, env = Pfedit.get_current_context () in
+ let evd, env = Pfedit.get_current_context () in (* XXX *)
let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
@@ -1519,7 +1521,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let env = Global.env() in
let evd = Evd.from_env env 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
+ let function_r = Sorts.Relevant in (* TODO relevance *)
+ let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot function_name function_r,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in
let evd = Evd.minimize_universes evd in
@@ -1537,7 +1540,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
match Constr.kind eq' with
| App(e,[|_;_;eq_fix|]) ->
- mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix))
+ mkLambda (make_annot (Name function_name) Sorts.Relevant,function_type,subst_var function_name (compose_lam res_vars eq_fix))
| _ -> failwith "Recursive Definition (res not eq)"
in
let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 07:51:05 +0000