/[mojave]
ViewVC logotype

Revision 3292


Jump to revision: Previous Next
Author: nogin
Date: Sun Jun 24 10:25:49 2001 UTC (20 years, 1 month ago)
Changed paths: 104 (showing only 100; show all)
Log Message:
*** IMPORTANT: before doing "cvs update" see warning below ***

This commit implements a global resource that brings together resource management
that used to be done by each resource in its own way.

- A much simplier object (Mp_resource.resource_info) is now needed to create a new resource.
Additionally, many resource helper modules, such as term_match_table now provide functions
that create a resource_info for you.

- Funtions get_tactic_arg, get_int_tactic_arg, etc were replaced by a single function
get_resource_arg (note: functions for basci types, such as get_with_arg, get_sel_args, etc
were _not_ affected)

- Resource declaration statement now declares and resource creation statement now creates
a function get_<name>_resource. This function ca be passed as a second argument
to get_resource_arg to retrieve the current value of a particular resource.

- Resource annotation functions are now separate from the resource declaration/creation
mechanism. Resource annotation on a rule are now passed to a function named
process_<name>_resource_annotation. This function must have the appropriate
Mp_resource.annotation_processor type for the resource. This function can be declared
and implemented in _any_ module, not just the module that declares and creates the
<name> resource.

- Currenlty MetaPRL leaves it to Ocaml to keep track of these functions.
Consequently the module that defines the process_<name>_resource_annotation function
must be open'ed (not included!) by modules that use <name> annotations.

-----

Unfinished business in this commit:
- Remainder of TODO 1.12 and 1.13

- Some proofs were broken by this commit. It appears that they were broken for
a "good" reason, but still need to be fixed.

- I need to make sure things now always have the right precedences (all things being equal,
the later an item is added to resource, the earlier precedence it should have).

- Consider adding refiner sentinels and display forms to global resource as well.
Currently each of them still does its own way of resource management (although the way
display forms are managed was changed by this commit - need to make sure the precedences
are right).

- Distributed refinement: I am afraid that the current resource code
will either work correctly only if all processes in the distributed group have
the same global resource, or it will attempt to pass around all the resource data.
Obviously, neither of these choices is a good one.

*** WARNING ***

This commit changes the tactic_arg type and also makes minor changes in
the FilterCache.info type. Because of that old .prlb and .cmoz files
*will no longer work*. Old .prla files will work, but will produce lots
of (harmless) Filter_summary.dest_term warning.

Before doing "cvs update" do the following:
1) export all your unsaved proofs into .prla files.
2) rm -f theories/*/*.prlb
3) run "make clean"


Changed paths

Path Details
Directorymetaprl/doc/htmlman/system/mp-conversionals.html modified , text changed
Directorymetaprl/doc/resources_spec.txt modified , text changed
Directorymetaprl/editor/ml/package_info.ml modified , text changed
Directorymetaprl/editor/ml/package_sig.mlz modified , text changed
Directorymetaprl/editor/ml/shell_rewrite.ml modified , text changed
Directorymetaprl/editor/ml/shell_rule.ml modified , text changed
Directorymetaprl/editor/ml/shell_state.ml modified , text changed
Directorymetaprl/filter/base/filter_ocaml.ml modified , text changed
Directorymetaprl/filter/base/filter_prog.ml modified , text changed
Directorymetaprl/filter/base/filter_summary.ml modified , text changed
Directorymetaprl/filter/base/filter_summary.mli modified , text changed
Directorymetaprl/filter/base/filter_type.ml modified , text changed
Directorymetaprl/filter/boot/conversionals_boot.ml modified , text changed
Directorymetaprl/filter/boot/proof_boot.ml modified , text changed
Directorymetaprl/filter/boot/proof_term_boot.ml modified , text changed
Directorymetaprl/filter/boot/proof_term_boot.mli modified , text changed
Directorymetaprl/filter/boot/sequent_boot.ml modified , text changed
Directorymetaprl/filter/boot/tactic_boot.ml modified , text changed
Directorymetaprl/filter/boot/tactic_boot_sig.mlz modified , text changed
Directorymetaprl/filter/filter/filter_parse.ml modified , text changed
Directorymetaprl/mk/preface modified , text changed
Directorymetaprl/mllib/red_black_table.ml modified , text changed
Directorymetaprl/mllib/set_sig.mlz modified , text changed
Directorymetaprl/mllib/splay_table.ml modified , text changed
Directorymetaprl/refiner/reflib/Files modified , text changed
Directorymetaprl/refiner/reflib/dform.ml modified , text changed
Directorymetaprl/refiner/reflib/dform.mli modified , text changed
Directorymetaprl/refiner/reflib/dform_print.ml modified , text changed
Directorymetaprl/refiner/reflib/dform_print.mli modified , text changed
Directorymetaprl/refiner/reflib/mp_resource.ml modified , text changed
Directorymetaprl/refiner/reflib/mp_resource.mli modified , text changed
Directorymetaprl/refiner/reflib/term_dtable.ml modified , text changed
Directorymetaprl/refiner/reflib/term_dtable.mli modified , text changed
Directorymetaprl/refiner/reflib/term_match_table.ml modified , text changed
Directorymetaprl/refiner/reflib/term_match_table.mli modified , text changed
Directorymetaprl/refiner/reflib/term_stable.ml modified , text changed
Directorymetaprl/refiner/reflib/term_stable.mli modified , text changed
Directorymetaprl/theories/base/base_auto_tactic.ml modified , text changed
Directorymetaprl/theories/base/base_auto_tactic.mli modified , text changed
Directorymetaprl/theories/base/base_cache.ml modified , text changed
Directorymetaprl/theories/base/base_cache.mli modified , text changed
Directorymetaprl/theories/base/base_dtactic.ml modified , text changed
Directorymetaprl/theories/base/base_dtactic.mli modified , text changed
Directorymetaprl/theories/base/typeinf.ml modified , text changed
Directorymetaprl/theories/base/typeinf.mli modified , text changed
Directorymetaprl/theories/czf/Makefile modified , text changed
Directorymetaprl/theories/czf/czf_itt_and.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_dall.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_dexists.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_empty.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_eq.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_false.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_implies.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_member.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_nat.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_or.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_power.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_rel.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_sall.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_sep.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_set.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_set_ind.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_sexists.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_singleton.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_subset.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_true.ml modified , text changed
Directorymetaprl/theories/fol/cfol_itt_and.ml modified , text changed
Directorymetaprl/theories/fol/cfol_itt_base.ml modified , text changed
Directorymetaprl/theories/fol/fol_and.ml modified , text changed
Directorymetaprl/theories/fol/fol_false.ml modified , text changed
Directorymetaprl/theories/fol/fol_implies.ml modified , text changed
Directorymetaprl/theories/fol/fol_not.ml modified , text changed
Directorymetaprl/theories/fol/fol_true.ml modified , text changed
Directorymetaprl/theories/itt/itt_bisect.ml modified , text changed
Directorymetaprl/theories/itt/itt_bool.ml modified , text changed
Directorymetaprl/theories/itt/itt_decidable.ml modified , text changed
Directorymetaprl/theories/itt/itt_decidable.mli modified , text changed
Directorymetaprl/theories/itt/itt_dprod.ml modified , text changed
Directorymetaprl/theories/itt/itt_equal.ml modified , text changed
Directorymetaprl/theories/itt/itt_equal.mli modified , text changed
Directorymetaprl/theories/itt/itt_esquash.ml modified , text changed
Directorymetaprl/theories/itt/itt_fun.ml modified , text changed
Directorymetaprl/theories/itt/itt_int_ext.ml modified , text changed
Directorymetaprl/theories/itt/itt_isect.ml modified , text changed
Directorymetaprl/theories/itt/itt_list2.ml modified , text changed
Directorymetaprl/theories/itt/itt_nat.ml modified , text changed
Directorymetaprl/theories/itt/itt_record.ml modified , text changed
Directorymetaprl/theories/itt/itt_record_label.ml modified , text changed
Directorymetaprl/theories/itt/itt_squash.ml modified , text changed
Directorymetaprl/theories/itt/itt_squash.mli modified , text changed
Directorymetaprl/theories/itt/itt_squash.prla modified , text changed
Directorymetaprl/theories/itt/itt_squiggle.ml modified , text changed
Directorymetaprl/theories/itt/itt_subtype.ml modified , text changed
Directorymetaprl/theories/itt/itt_subtype.mli modified , text changed
Directorymetaprl/theories/itt/itt_void.ml modified , text changed
Directorymetaprl/theories/itt/itt_well_founded.ml modified , text changed
Directorymetaprl/theories/reflect_itt/refl_free_vars.ml modified , text changed
Directorymetaprl/theories/tactic/mptop.ml modified , text changed
Directorymetaprl/theories/tactic/mptop.mli modified , text changed
Directorymetaprl/theories/tactic/tactic_cache.ml modified , text changed
[...]

  ViewVC Help
Powered by ViewVC 1.1.26