diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-29 15:35:45 +0200 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-29 15:56:18 +0200 |
commit | e969a56e2d0c354057b4d9da0d48349d2a5a61e2 (patch) | |
tree | a34ce5ef80fd65ec874d265a3dc48ccd0b75743c /plugins | |
parent | 2c513c07473b40c390dc1e1d24bfaf971c685514 (diff) |
CLEANUP: taking advantage of "_ % _" operator to express function composition in a more obvious way
This commit rewrites terms
(fun x -> f1 (f2 ... (fN x)...))
to
f1 % f2 % ... % fN
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 22 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 4 |
2 files changed, 13 insertions, 13 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f47ab2616..04c2c51e7 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -940,8 +940,8 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl decl = Nameops.out_name (RelDecl.get_name decl) -let var_of_decl decl = mkVar (id_of_decl decl) +let id_of_decl = Nameops.out_name % RelDecl.get_name +let var_of_decl = mkVar % id_of_decl let revert idl = tclTHEN (Proofview.V82.of_tactic (generalize (List.map mkVar idl))) @@ -1121,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl))) + prlist_with_sep spc (Ppconstr.pr_id % Nameops.out_name % RelDecl.get_name) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl))) + prlist_with_sep spc (Ppconstr.pr_id % Nameops.out_name % RelDecl.get_name) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1279,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (fun decl -> Nameops.out_name (RelDecl.get_name decl)) princ_params)) + (args_id@(List.map (Nameops.out_name % RelDecl.get_name) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs @@ -1558,7 +1558,7 @@ let prove_principle_for_gen | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) - let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in + let subst_constrs = List.map (mkVar % Nameops.out_name % get_name) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in @@ -1586,7 +1586,7 @@ let prove_principle_for_gen ) g in - let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in + let args_ids = List.map (Nameops.out_name % get_name) princ_info.args in let lemma = match !tcc_lemma_ref with | None -> error "No tcc proof !!" @@ -1633,7 +1633,7 @@ let prove_principle_for_gen [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (fun decl -> Nameops.out_name (get_name decl)) + (List.rev_map (Nameops.out_name % get_name) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by @@ -1671,7 +1671,7 @@ let prove_principle_for_gen in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = - List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates + List.map (Nameops.out_name % get_name) princ_info.predicates in let pte_info = { proving_tac = @@ -1687,7 +1687,7 @@ let prove_principle_for_gen is_mes acc_inv fix_id (!tcc_list@(List.map - (fun decl -> (Nameops.out_name (get_name decl))) + (Nameops.out_name % get_name) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) @@ -1716,7 +1716,7 @@ let prove_principle_for_gen (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof - (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches) + (List.map (Nameops.out_name % get_name) princ_info.branches) (List.rev args_ids) ) gl' diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index d9933cf41..f8aa21e95 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -59,8 +59,8 @@ let understand = Pretyping.understand (Global.env()) Evd.empty let id_of_name = function Anonymous -> Id.of_string "H" | Name id -> id;; -let name_of_string str = Name (Id.of_string str) -let string_of_name nme = Id.to_string (id_of_name nme) +let name_of_string = Name.mk_name % Id.of_string +let string_of_name = Id.to_string % id_of_name (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = |