/[mojave]/metaprl/theories/itt/itt_int_ext.ml
ViewVC logotype

Log of /metaprl/theories/itt/itt_int_ext.ml

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 7950)

Revision 3586 - (view) (download) (annotate) - [select for diffs]
Modified Sat Apr 27 01:42:23 2002 UTC (19 years, 1 month ago) by nogin
File length: 17317 byte(s)
Diff to previous 3442
Noop commit - I've only fixed the CRLF/LF mixed line terminators.


Revision 3442 - (view) (download) (annotate) - [select for diffs]
Modified Thu Nov 15 20:25:28 2001 UTC (19 years, 7 months ago) by yegor
File length: 17317 byte(s)
Diff to previous 3361
Itt_int_ext: more conversions added to reduce resource

Itt_int_arih: first working version of arithT!!!
You can observe proof of test rule and try to replace it with just arithT
in the root.
While now arithT knows only numbers, variables and +


Revision 3361 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 5 03:26:02 2001 UTC (19 years, 10 months ago) by emre
File length: 17152 byte(s)
Diff to previous 3354
I've added display forms for le_bool, gt_bool, and
ge_bool. The forms for beq_int, bneq_int, and lt_bool
were used as a model.  They appear to work fine, but
someone should probably still check them to make sure
that the details are ok.


Revision 3354 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 1 18:52:04 2001 UTC (19 years, 10 months ago) by emre
File length: 16727 byte(s)
Diff to previous 3352
Added reductions for the boolean comparisons to the reduce tactic.


Revision 3352 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 1 13:24:09 2001 UTC (19 years, 10 months ago) by nogin
File length: 16529 byte(s)
Diff to previous 3329
- Made sure conditional rewrites are added to toploop the same way the normal
rules and rewrites are.
- Added <<if ... then ... else ...>> term syntax macro (stands for iftenelse{ ; ; })
- Proved and added to reduceC the reduction for ind with constant argument (as Brian
requested). This reduction does everything except incrementing/decrementing the number
(it will leave if as n + 1 or n - 1).
- Fixed lt_bool reduction


Revision 3329 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 13 21:34:19 2001 UTC (19 years, 11 months ago) by nogin
File length: 17051 byte(s)
Diff to previous 3292
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theories.


Revision 3292 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 10:25:49 2001 UTC (19 years, 11 months ago) by nogin
File length: 16811 byte(s)
Diff to previous 3281
*** 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"


Revision 3281 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 13:56:53 2001 UTC (20 years ago) by nogin
File length: 16796 byte(s)
Diff to previous 3279
The redundant "_resource" suffix should not be used in resource names.


Revision 3279 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 11:48:09 2001 UTC (20 years ago) by nogin
File length: 16895 byte(s)
Diff to previous 3276
- Renamed andthenC -> thenC
- Added byDefT : conv -> tactic
- Proved rewrites in Itt_dprod
- Removed some unused stuff from one of the filter_prog interfaces.


Revision 3276 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 19 15:17:10 2001 UTC (20 years ago) by nogin
File length: 16901 byte(s)
Diff to previous 3257
Added support for the following syntax of resource improvement:
let resource name += expr
and
let resource name += [ expr1; expr2; ...; exprn ]


Revision 3257 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 13 19:32:30 2001 UTC (20 years ago) by kopylov
File length: 16981 byte(s)
Diff to previous 3247
1. I added new primitive rules:
     Itt_struct.exchange
     Itt_pointwise.hypSubstPointwise
     Itt_pointwise.contextSubstPointwise

   The last two rules show the differences between pointwise and pairwise functionality.
   They are valid in pointwise functionality (as well as quoationtElimination2).

2. Itt_struct3 contains some rules that derived from these new ones.
   But thesd rules are valid in both functionalities.

3. I moved definition of natural numbers to a new theory Itt_nat.
   To prove induction for natural numbers one needs Itt_struct3.
   I almost proved it (leaving some simple arithmetic subgoals, that should
   be killed by arith)

4. I defined record type.
   Itt_record is a main theory of records.
   Itt_record_exm contains some examples.

5. I add a new conversion
        * applyAllC : conv list -> conv
   that applies all conversions to all subterms and a tactic
        * rwa : conv list -> int -> tactic
        = rw (applyAllC convs)


Revision 3247 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 1 21:36:46 2001 UTC (20 years ago) by kopylov
File length: 17649 byte(s)
Diff to previous 3246
*** empty log message ***


Revision 3246 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 1 20:57:31 2001 UTC (20 years ago) by kopylov
File length: 17983 byte(s)
Diff to previous 3223
- The theory ctt_markov (Constructive type theory with Markov
  Principle) is added.

- Some definitions and simple facts are added to itt_int_ext


Revision 3223 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 23:59:11 2001 UTC (20 years, 1 month ago) by nogin
File length: 16243 byte(s)
Diff to previous 3207
Finally, I am able to commit what I was getting to
in all these commits over the last several days.

I changed the parser to index declared opnames by its "shape" -
last string of opname + parameter types + subterm arities
instead of just the last string (as it used to be). This means that
the parser now checks whether the usage of an opname corresponds
to its declaration. This allowed me to detect numerous typos in
display forms and even some rules and rewrites and, hopefully,
will prevent people from making such typos in the future.

This is only the first pass of the implementation. I still need to:
- make sure none of my fixes broke any display forms that used to work
  because of typos cancelling each other
- update the documentation
- implement checking of shapes on the opnames specified using the
  Module!name notation (currently no checking is done on such opnames)


Revision 3207 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 4 08:45:12 2001 UTC (20 years, 1 month ago) by yegor
File length: 16254 byte(s)
Diff to previous 3163
1.Some minor changes in old files
2.First ugly approach to Arith implementation. It just can find contradiction
  and construct contradictory inequality. Next step will be polynoms and
  inequalities normalization. It will increase range of input inequalities and
  let easily prove resulting contradictory inequality.


Revision 3163 - (view) (download) (annotate) - [select for diffs]
Modified Fri Mar 2 13:56:49 2001 UTC (20 years, 3 months ago) by yegor
File length: 15858 byte(s)
Diff to previous 3159
~-rules are duplicated by appropriate rewrites


Revision 3159 - (view) (download) (annotate) - [select for diffs]
Modified Sat Feb 24 13:04:46 2001 UTC (20 years, 3 months ago) by nogin
File length: 13043 byte(s)
Diff to previous 3151
- Fixed a nasty bug in indEquality. Yegor, can you dbl-check, please?
- Renamed "uni_minus" to "minus".
- << (- 'a) >> is now parsed correctly as minus{'a} instead of sub{'a}.
- Rewrote Yegor's theories to use the parser shortcut for "minus".
- Fixed the minus_df.


Revision 3151 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 21 13:58:17 2001 UTC (20 years, 4 months ago) by yegor
File length: 13069 byte(s)
Diff to previous 3091
1.Display forms taken from old itt_int
2.meta-evaluation on constants taken from old itt_int
3.Some proofs added, "terrible" elim-rule fixed once again


Revision 3091 - (view) (download) (annotate) - [select for diffs]
Modified Wed Dec 13 12:04:15 2000 UTC (20 years, 6 months ago) by yegor
File length: 9409 byte(s)
Diff to previous 3085
Moved from old style conditional rewrites to rules with '~' operator instead of '<-->'.
Just now all reduce resources are commented out.


Revision 3085 - (view) (download) (annotate) - [select for diffs]
Modified Wed Oct 18 21:32:01 2000 UTC (20 years, 8 months ago) by nogin
File length: 7786 byte(s)
Diff to previous 3084
Fixed Yegor's typos that prevented MetaPRL from staring (Yegor, please
take a look at my changes)

Other minor fixes.


Revision 3084 - (view) (download) (annotate) - [select for diffs]
Modified Wed Oct 11 05:28:11 2000 UTC (20 years, 8 months ago) by yegor
File length: 7740 byte(s)
Diff to previous 3083
A couple of rewrites turn from primitive to interative


Revision 3083 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 10 12:29:43 2000 UTC (20 years, 8 months ago) by yegor
File length: 7726 byte(s)
Diff to previous 3081
reduce_resources added and theories added to Makefile


Revision 3081 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 6 17:17:39 2000 UTC (20 years, 8 months ago) by yegor
File length: 7283 byte(s)
Diff to previous 3061
some documenting markup and resource annotation added


Revision 3061 - (view) (download) (annotate) - [select for diffs]
Added Tue Sep 12 07:56:23 2000 UTC (20 years, 9 months ago) by yegor
File length: 5559 byte(s)
itt_int_bool_new was split into itt_int_base (beq_int, lt_bool, lt, add, uni_minus, sub, int, ind, number)
and itt_int_ext (ge_bool, le_bool, gt_bool, ge, le, gt, mul, div, rem)


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26