summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/functional_principles_proofs.ml23
-rw-r--r--contrib/funind/functional_principles_types.ml32
-rw-r--r--contrib/funind/g_indfun.ml4125
-rw-r--r--contrib/funind/indfun.ml4
-rw-r--r--contrib/funind/indfun_common.ml7
-rw-r--r--contrib/funind/invfun.ml8
-rw-r--r--contrib/funind/merge.ml4
-rw-r--r--contrib/funind/rawterm_to_relation.ml16
-rw-r--r--contrib/funind/recdef.ml8
9 files changed, 151 insertions, 76 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index bd335d30..9f3e412a 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -136,7 +136,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
fun g ->
let prov_id = pf_get_new_id hyp_id g in
tclTHENS
- ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
+ ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
[tclTHENLIST
[
(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
in
(* observe_tac "rec hyp " *)
(tclTHENS
- (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
+ (assert_tac (Name rec_pte_id) t_x)
[
(* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
(* observe_tac "prove rec hyp" *)
@@ -571,7 +571,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
fun g ->
let prov_hid = pf_get_new_id hid g in
tclTHENLIST[
- forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+ pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
thin [hid];
h_rename [prov_hid,hid]
] g
@@ -1347,7 +1347,7 @@ let build_clause eqs =
{
Tacexpr.onhyps =
Some (List.map
- (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp)
+ (fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
eqs
);
Tacexpr.concl_occs = Rawterm.no_occurrences_expr
@@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
false
(true,5)
[Lazy.force refl_equal]
- [Auto.Hint_db.empty false]
+ [Auto.Hint_db.empty empty_transparent_state false]
)
)
)
@@ -1495,10 +1495,9 @@ let prove_principle_for_gen
((* observe_tac "prove_rec_arg_acc" *)
(tclCOMPLETE
(tclTHEN
- (forward
- (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
- (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
- (mkApp (delayed_force well_founded,[|input_type;relation|])))
+ (assert_by (Name wf_thm_id)
+ (mkApp (delayed_force well_founded,[|input_type;relation|]))
+ (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
(
(* observe_tac *)
(* "apply wf_thm" *)
@@ -1559,10 +1558,10 @@ let prove_principle_for_gen
(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
(princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
);
- (* observe_tac "" *) (forward
- (Some (prove_rec_arg_acc))
- (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
+ (* observe_tac "" *) (assert_by
+ (Name acc_rec_arg_id)
(mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+ (prove_rec_arg_acc)
);
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *)
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 16076479..b03bdf31 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -552,13 +552,31 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
| _ -> anomaly ""
in
let (_,(const,_,_)) =
- build_functional_principle false
- first_type
- (Array.of_list sorts)
- this_block_funs
- 0
- (prove_princ_for_struct false 0 (Array.of_list funs))
- (fun _ _ _ -> ())
+ try
+ build_functional_principle false
+ first_type
+ (Array.of_list sorts)
+ this_block_funs
+ 0
+ (prove_princ_for_struct false 0 (Array.of_list funs))
+ (fun _ _ _ -> ())
+ with e ->
+ begin
+ begin
+ try
+ let id = Pfedit.get_current_proof_name () in
+ let s = string_of_id id in
+ let n = String.length "___________princ_________" in
+ if String.length s >= n
+ then if String.sub s 0 n = "___________princ_________"
+ then Pfedit.delete_current_proof ()
+ else ()
+ else ()
+ with _ -> ()
+ end;
+ raise (Defining_principle e)
+ end
+
in
incr i;
let opacity =
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index d435f513..a79b46d9 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
+open Util
open Term
open Names
open Pp
@@ -128,25 +129,52 @@ ARGUMENT EXTEND auto_using'
| [ ] -> [ [] ]
END
+let pr_rec_annotation2_aux s r id l =
+ str ("{"^s^" ") ++ Ppconstr.pr_constr_expr r ++
+ Util.pr_opt Nameops.pr_id id ++
+ Pptactic.pr_auto_using Ppconstr.pr_constr_expr l ++ str "}"
+
+let pr_rec_annotation2 = function
+ | Struct id -> str "{struct" ++ Nameops.pr_id id ++ str "}"
+ | Wf(r,id,l) -> pr_rec_annotation2_aux "wf" r id l
+ | Mes(r,id,l) -> pr_rec_annotation2_aux "measure" r id l
+
VERNAC ARGUMENT EXTEND rec_annotation2
+PRINTED BY pr_rec_annotation2
[ "{" "struct" ident(id) "}"] -> [ Struct id ]
| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ]
END
+let pr_binder2 (idl,c) =
+ str "(" ++ Util.prlist_with_sep spc Nameops.pr_id idl ++ spc () ++
+ str ": " ++ Ppconstr.pr_lconstr_expr c ++ str ")"
VERNAC ARGUMENT EXTEND binder2
- [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] ->
- [
- LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ]
+PRINTED BY pr_binder2
+ [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> [ (idl,c) ]
END
+let make_binder2 (idl,c) =
+ LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c)
+
+let pr_rec_definition2 (id,bl,annot,type_,def) =
+ Nameops.pr_id id ++ spc () ++ Util.prlist_with_sep spc pr_binder2 bl ++
+ Util.pr_opt pr_rec_annotation2 annot ++ spc () ++ str ":" ++ spc () ++
+ Ppconstr.pr_lconstr_expr type_ ++ str " :=" ++ spc () ++
+ Ppconstr.pr_lconstr_expr def
VERNAC ARGUMENT EXTEND rec_definition2
- [ ident(id) binder2_list( bl)
- rec_annotation2_opt(annot) ":" lconstr( type_)
+PRINTED BY pr_rec_definition2
+ [ ident(id) binder2_list(bl)
+ rec_annotation2_opt(annot) ":" lconstr(type_)
":=" lconstr(def)] ->
- [let names = List.map snd (Topconstr.names_of_local_assums bl) in
+ [ (id,bl,annot,type_,def) ]
+END
+
+let make_rec_definitions2 (id,bl,annot,type_,def) =
+ let bl = List.map make_binder2 bl in
+ let names = List.map snd (Topconstr.names_of_local_assums bl) in
let check_one_name () =
if List.length names > 1 then
Util.user_err_loc
@@ -173,52 +201,73 @@ VERNAC ARGUMENT EXTEND rec_definition2
| Some an ->
check_exists_args an
in
- ((Util.dummy_loc,id), ni, bl, type_, def) ]
- END
-
-
-VERNAC ARGUMENT EXTEND rec_definitions2
-| [ rec_definition2(rd) ] -> [ [rd] ]
-| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ]
-END
+ ((Util.dummy_loc,id), ni, bl, type_, def)
VERNAC COMMAND EXTEND Function
- ["Function" rec_definitions2(recsl)] ->
+ ["Function" ne_rec_definition2_list_sep(recsl,"with")] ->
[
- do_generate_principle false recsl;
+ do_generate_principle false (List.map make_rec_definitions2 recsl);
]
END
+let pr_fun_scheme_arg (princ_name,fun_name,s) =
+ Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
+ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
+ Ppconstr.pr_rawsort s
VERNAC ARGUMENT EXTEND fun_scheme_arg
+PRINTED BY pr_fun_scheme_arg
| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
END
-VERNAC ARGUMENT EXTEND fun_scheme_args
-| [ fun_scheme_arg(fa) ] -> [ [fa] ]
-| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas]
-END
+
+let warning_error names e =
+ match e with
+ | Building_graph e ->
+ Pp.msg_warning
+ (str "Cannot define graph(s) for " ++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+ if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+ | Defining_principle e ->
+ Pp.msg_warning
+ (str "Cannot define principle(s) for "++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+ if do_observe () then Cerrors.explain_exn e else mt ())
+ | _ -> anomaly ""
+
VERNAC COMMAND EXTEND NewFunctionalScheme
- ["Functional" "Scheme" fun_scheme_args(fas) ] ->
+ ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] ->
[
- try
- Functional_principles_types.build_scheme fas
- with Functional_principles_types.No_graph_found ->
- match fas with
- | (_,fun_name,_)::_ ->
- begin
- begin
- make_graph (Nametab.global fun_name)
- end
- ;
- try Functional_principles_types.build_scheme fas
- with Functional_principles_types.No_graph_found ->
- Util.error ("Cannot generate induction principle(s)")
- end
- | _ -> assert false (* we can only have non empty list *)
+ begin
+ try
+ Functional_principles_types.build_scheme fas
+ with Functional_principles_types.No_graph_found ->
+ begin
+ match fas with
+ | (_,fun_name,_)::_ ->
+ begin
+ begin
+ make_graph (Nametab.global fun_name)
+ end
+ ;
+ try Functional_principles_types.build_scheme fas
+ with Functional_principles_types.No_graph_found ->
+ Util.error ("Cannot generate induction principle(s)")
+ | e ->
+ let names = List.map (fun (_,na,_) -> na) fas in
+ warning_error names e
+
+ end
+ | _ -> assert false (* we can only have non empty list *)
+ end
+ | e ->
+ let names = List.map (fun (_,na,_) -> na) fas in
+ warning_error names e
+
+ end
]
END
(***** debug only ***)
@@ -307,9 +356,9 @@ let mkEq typ c1 c2 =
let poseq_unsafe idunsafe cstr gl =
let typ = Tacmach.pf_type_of gl cstr in
tclTHEN
- (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
+ (Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
(tclTHENFIRST
- (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr))
+ (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr))
Tactics.reflexivity)
gl
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 79ef0097..b6b2cbd1 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -168,7 +168,7 @@ let build_newrecursive
if Impargs.is_implicit_args()
then Impargs.compute_implicits env0 arity
else [] in
- let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in
+ let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
(Environ.push_named (recname,None,arity) env, impls'))
(env0,[]) lnameargsardef in
let recdef =
@@ -612,7 +612,9 @@ let rec add_args id new_args b =
CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
| CCast(loc,b1,CastCoerce) ->
CCast(loc,add_args id new_args b1,CastCoerce)
+ | CRecord _ -> anomaly "add_args : CRecord"
| CNotation _ -> anomaly "add_args : CNotation"
+ | CGeneralization _ -> anomaly "add_args : CGeneralization"
| CPrim _ -> b
| CDelimiters _ -> anomaly "add_args : CDelimiters"
| CDynamic _ -> anomaly "add_args : CDynamic"
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 4010b49d..a3c169b7 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -238,20 +238,19 @@ let with_full_print f a =
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
let old_rawprint = !Flags.raw_print in
- let old_dump = !Flags.dump in
Flags.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
Impargs.make_contextual_implicit_args false;
Impargs.make_contextual_implicit_args false;
- Flags.dump := false;
+ Dumpglob.pause ();
try
let res = f a in
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
- Flags.dump := old_dump;
+ Dumpglob.continue ();
res
with
| e ->
@@ -259,7 +258,7 @@ let with_full_print f a =
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
- Flags.dump := old_dump;
+ Dumpglob.continue ();
raise e
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index f62d70ab..5c8f0871 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -445,10 +445,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
in
tclTHENSEQ
[ observe_tac "intro args_names" (tclMAP h_intro args_names);
- observe_tac "principle" (forward
- (Some (h_exact f_principle))
- (dummy_loc,Genarg.IntroIdentifier principle_id)
- princ_type);
+ observe_tac "principle" (assert_by
+ (Name principle_id)
+ princ_type
+ (h_exact f_principle));
tclTHEN_i
(observe_tac "functional_induction" (
fun g ->
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index ec456aae..9bbd165d 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -855,7 +855,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
[rawlist], named ident.
FIXME: params et cstr_expr (arity) *)
let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
- (rawlist:(identifier * rawconstr) list):inductive_expr =
+ (rawlist:(identifier * rawconstr) list) =
let lident = dummy_loc, shift.ident in
let bindlist , cstr_expr = (* params , arities *)
merge_rec_params_and_arity prms1 prms2 shift mkSet in
@@ -863,7 +863,7 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
List.map (* zeta_normalize t ? *)
(fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
rawlist in
- lident , bindlist , cstr_expr , lcstor_expr
+ lident , bindlist , Some cstr_expr , lcstor_expr
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 08a97fd2..09b7fbdf 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1192,7 +1192,7 @@ let do_build_inductive
let rel_ind i ext_rel_constructors =
((dummy_loc,relnames.(i)),
rel_params,
- rel_arities.(i),
+ Some rel_arities.(i),
ext_rel_constructors),None
in
let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
@@ -1224,9 +1224,14 @@ let do_build_inductive
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
+ let repacked_rel_inds =
+ List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+ rel_inds
+ in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,repacked_rel_inds))
+ ++ fnl () ++
msg
in
observe (msg);
@@ -1234,9 +1239,14 @@ let do_build_inductive
| e ->
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
+ let repacked_rel_inds =
+ List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+ rel_inds
+ in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,repacked_rel_inds))
+ ++ fnl () ++
Cerrors.explain_exn e
in
observe msg;
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 5bd7a6b2..6dc0d5bf 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: recdef.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: recdef.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
open Term
open Termops
@@ -740,7 +740,6 @@ let termination_proof_header is_mes input_type ids args_id relation
(observe_tac
"first assert"
(assert_tac
- true (* the assert thm is in first subgoal *)
(Name wf_rec_arg)
(mkApp (delayed_force acc_rel,
[|input_type;relation;mkVar rec_arg_id|])
@@ -753,7 +752,6 @@ let termination_proof_header is_mes input_type ids args_id relation
(observe_tac
"second assert"
(assert_tac
- true
(Name wf_thm)
(mkApp (delayed_force well_founded,[|input_type;relation|]))
)
@@ -1157,12 +1155,12 @@ let rec introduce_all_values_eq cont_tac functional termine
[] ->
let heq2 = next_global_ident_away true heq_id ids in
tclTHENLIST
- [forward None (dummy_loc,IntroIdentifier heq2)
+ [pose_proof (Name heq2)
(mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
simpl_iter (onHyp heq2);
unfold_in_hyp [((true,[1]), evaluable_of_global_reference
(global_of_constr functional))]
- ((all_occurrences_expr, heq2), Tacexpr.InHyp);
+ ((all_occurrences_expr, heq2), InHyp);
tclTHENS
(fun gls ->
let t_eq = compute_renamed_type gls (mkVar heq2) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 21:39:03 +0000