]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years agoTrick: the refiner always subst-expands the outtype, so that the beta-redex
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 16:37:40 +0000 (16:37 +0000)]
Trick: the refiner always subst-expands the outtype, so that the beta-redex
that will be formed will always be reduced by substitution.

15 years agoBug fixed in two lines + 5 lines of comment.
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 16:16:59 +0000 (16:16 +0000)]
Bug fixed in two lines + 5 lines of comment.
During select, the context of the goal is changed and the conclusion
is changed too (too a ?[out_scope]). Then the changed conclusion was
relocated in the changed context, triggering a delift that in turn triggered
the unification case "something vs ?[out_of_scope]"... at the bad time!
Fixed by manually relocating the new conclusion in the new context.
Manually means opening and building again the cic_term data type, which is
ugly and sort of fragile.

15 years agoassert_tac now takes a list of sequents and also checks that the number of
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 13:36:39 +0000 (13:36 +0000)]
assert_tac now takes a list of sequents and also checks that the number of
sequents is the appropriate one.

It is the first example of a high-tactic that works also with the stack.

15 years agoNew debugging tactic nassert:
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 12:44:31 +0000 (12:44 +0000)]
New debugging tactic nassert:

 nassert H1: t1 ... Hn: tn \vdash T

asserts (using OCaml's assert) that the current goal is equal (using
OCaml equality) to the one given the user. The substitution is fully
expanded just before calling OCaml equality.

15 years agoSemantic selection back again (but no semantic cut&paste yet).
Claudio Sacerdoti Coen [Sun, 12 Apr 2009 11:06:17 +0000 (11:06 +0000)]
Semantic selection back again (but no semantic cut&paste yet).

15 years agoMatch is now rendered as best as possible.
Claudio Sacerdoti Coen [Sun, 12 Apr 2009 10:56:31 +0000 (10:56 +0000)]
Match is now rendered as best as possible.

15 years agoThe sequent viewer now considers the context to render the Rels.
Claudio Sacerdoti Coen [Fri, 10 Apr 2009 13:19:11 +0000 (13:19 +0000)]
The sequent viewer now considers the context to render the Rels.

15 years ago- character: we adjusted some "autobatch" parameters
Ferruccio Guidi [Thu, 9 Apr 2009 18:59:12 +0000 (18:59 +0000)]
- character: we adjusted some "autobatch" parameters
- limits: in classes and subssets we now ensure the compatibility between the
  inhabitance predicate and the equivalence relation

15 years agoThe substitution is now taken in account when printing sequents in the
Claudio Sacerdoti Coen [Thu, 9 Apr 2009 17:50:35 +0000 (17:50 +0000)]
The substitution is now taken in account when printing sequents in the
sequent viewer. Context is not yet taken in account.

15 years agoadded letin, still broken
Enrico Tassi [Thu, 9 Apr 2009 16:16:26 +0000 (16:16 +0000)]
added letin, still broken

15 years ago...
Enrico Tassi [Thu, 9 Apr 2009 16:16:04 +0000 (16:16 +0000)]
...

15 years agonew tactic whd implemented
Enrico Tassi [Thu, 9 Apr 2009 15:25:37 +0000 (15:25 +0000)]
new tactic whd implemented

15 years ago- change implemented in 4 lines
Enrico Tassi [Thu, 9 Apr 2009 15:05:29 +0000 (15:05 +0000)]
- change implemented in 4 lines
- select0 runs on hypothesis
- relocate honors conversion (but clearbody is not implemented)

15 years ago- generalize finished
Enrico Tassi [Thu, 9 Apr 2009 13:09:58 +0000 (13:09 +0000)]
- generalize finished
- relocate implemented in terms of delift

15 years ago?_OS1 := C[ ?_IN ]
Enrico Tassi [Thu, 9 Apr 2009 13:09:16 +0000 (13:09 +0000)]
?_OS1 := C[ ?_IN ]
?_IN := m
=======================
?[m;m]  =?=  ?_OS1

used to yield ? := Rel 2 instead of Rel 1, since the first m
was still out of scope when recursion reaches ?_IN

15 years agofixed modules order
Enrico Tassi [Thu, 9 Apr 2009 10:46:26 +0000 (10:46 +0000)]
fixed modules order

15 years agominor fixes
Enrico Tassi [Thu, 9 Apr 2009 09:47:05 +0000 (09:47 +0000)]
minor fixes

15 years ago...
Enrico Tassi [Thu, 9 Apr 2009 09:31:01 +0000 (09:31 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Thu, 9 Apr 2009 09:22:01 +0000 (09:22 +0000)]
...

15 years ago+ Chain NCic.term -> content -> presentation very very roughly implemented
Claudio Sacerdoti Coen [Thu, 9 Apr 2009 09:20:41 +0000 (09:20 +0000)]
+ Chain  NCic.term -> content -> presentation very very roughly implemented
+ The sequent viewer now prints also the neq sequents

15 years agoJust to make it compile again.
Claudio Sacerdoti Coen [Wed, 8 Apr 2009 16:31:56 +0000 (16:31 +0000)]
Just to make it compile again.

15 years agogeneralized is half-implemented (still broken)
Enrico Tassi [Wed, 8 Apr 2009 14:18:33 +0000 (14:18 +0000)]
generalized is half-implemented (still broken)

15 years agoAnalizyng the inductive type of the eliminated term and
Enrico Tassi [Wed, 8 Apr 2009 13:15:49 +0000 (13:15 +0000)]
Analizyng the inductive type of the eliminated term and
the sort of the goals are performed by tactics having
a side-effect. This allows to write tactics like elim and cases
as lists of tactics blocked together.

15 years ago- nrewrite ((very?) rough implementation)
Claudio Sacerdoti Coen [Tue, 7 Apr 2009 22:23:31 +0000 (22:23 +0000)]
- nrewrite ((very?) rough implementation)

  PATTERNS DO NOT WORK (why?)

15 years ago- more progress towards generalize, but I am stuck now
Claudio Sacerdoti Coen [Tue, 7 Apr 2009 21:55:14 +0000 (21:55 +0000)]
- more progress towards generalize, but I am stuck now
- elim completed (up to saturation)

15 years ago- select_tac honors the hypotheses pattern when required to generalize them
Enrico Tassi [Tue, 7 Apr 2009 17:23:10 +0000 (17:23 +0000)]
- select_tac honors the hypotheses pattern when required to generalize them
- clear [names]
- initial generalize tac implementation

15 years agoselect honors the substitution
Enrico Tassi [Tue, 7 Apr 2009 17:21:41 +0000 (17:21 +0000)]
select honors the substitution

15 years agoNew tactic clear; new syntax # _; to introduce and immediately clear an
Claudio Sacerdoti Coen [Mon, 6 Apr 2009 20:40:43 +0000 (20:40 +0000)]
New tactic clear; new syntax # _; to introduce and immediately clear an
hypothesis.

15 years ago...
Claudio Sacerdoti Coen [Mon, 6 Apr 2009 19:59:21 +0000 (19:59 +0000)]
...

15 years agotactic cases works! delift clears tags
Enrico Tassi [Mon, 6 Apr 2009 17:03:55 +0000 (17:03 +0000)]
tactic cases works! delift clears tags

15 years agoeta-contraction was made on the wrong term
Enrico Tassi [Mon, 6 Apr 2009 15:50:28 +0000 (15:50 +0000)]
eta-contraction was made on the wrong term

15 years agounification:
Enrico Tassi [Mon, 6 Apr 2009 15:43:14 +0000 (15:43 +0000)]
unification:
 - the case

    (? args) v.s. ?(tag:OUT_SCOPE)

   is considered as a pattern-driven delifting.
 - the case ? args v.s. t is reduced to ?[args] v.s. t
 - eta-contraction reimplemented
 - beta-expand no longer used

delift:
 - handle out/in scope tag

ntactics:
 - elim sets the out_scope tag for 1 entry

15 years agobetter error message
Enrico Tassi [Mon, 6 Apr 2009 15:35:59 +0000 (15:35 +0000)]
better error message

15 years agoadded one exception
Enrico Tassi [Mon, 6 Apr 2009 15:35:27 +0000 (15:35 +0000)]
added one exception

15 years ago- external quantification removed (will be reintroduced when needed)
Ferruccio Guidi [Mon, 6 Apr 2009 14:20:51 +0000 (14:20 +0000)]
- external quantification removed (will be reintroduced when needed)
- preamble added (was missing)

15 years agolimits: reorganized and attached to nightly tests (cow compiles fully)
Ferruccio Guidi [Mon, 6 Apr 2009 12:42:56 +0000 (12:42 +0000)]
limits: reorganized and attached to nightly tests (cow compiles fully)

15 years agosnapshot
Enrico Tassi [Mon, 6 Apr 2009 09:01:59 +0000 (09:01 +0000)]
snapshot

15 years ago- Procedural: now we generate the exact tactic (in place of some apply tactics) and...
Ferruccio Guidi [Sun, 5 Apr 2009 23:38:16 +0000 (23:38 +0000)]
- Procedural: now we generate the exact tactic (in place of some apply tactics) and we do not perform conversion steps before it (1104 change tactics omitted in the lambda-delta devel)
- new target for the PREDICATIVE-TOPOLOGY devel: now is "limits"

15 years ago...
Enrico Tassi [Thu, 2 Apr 2009 14:43:52 +0000 (14:43 +0000)]
...

15 years agoNew file nTacStatus to:
Enrico Tassi [Thu, 2 Apr 2009 14:15:36 +0000 (14:15 +0000)]
New file nTacStatus to:
 1) collect type declarations and utility functions
 2) make cic_term as abstract as possible

15 years agoadded analyse_indty
Enrico Tassi [Thu, 2 Apr 2009 10:50:23 +0000 (10:50 +0000)]
added analyse_indty

15 years agoNew tactic "case1_tac" that make "intro" followed by case of the first
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 22:37:06 +0000 (22:37 +0000)]
New tactic "case1_tac" that make "intro" followed by case of the first
argument.

It is now possible to write things like:

napply t; ## [ #H | *W; #K1 #K2 ]

15 years ago...
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 20:58:50 +0000 (20:58 +0000)]
...

15 years ago## prefix is now used for tinycals
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 20:53:04 +0000 (20:53 +0000)]
## prefix is now used for tinycals

Example:  napply H; ##[ #H | #K];

15 years agoNew tactic intro. Syntax: "# n".
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 20:40:51 +0000 (20:40 +0000)]
New tactic intro. Syntax: "# n".

15 years agoadded tentative elim
Enrico Tassi [Wed, 1 Apr 2009 16:41:20 +0000 (16:41 +0000)]
added tentative elim

15 years ago1) mk_meta now returns also the index of the created meta
Enrico Tassi [Wed, 1 Apr 2009 15:28:33 +0000 (15:28 +0000)]
1) mk_meta now returns also the index of the created meta
2) added datatypes for new patterns
3) added tactic nchange (using new patterns)
4) changed the type lowtac so that they no longer return the
   lists of open and closed goals, that are always computable
   in the new system
5) added some wrappers for kernel/refinement functions that
   work on statuses and terms labelled with their context
6) new implementation of select that performs subst-expansion.
   in-scope/out-scope used to mark regions selected by the pattern
7) ugly implementation of change based on re-opening of tagged
   subst entries

15 years agoremoved spurious "
Enrico Tassi [Wed, 1 Apr 2009 15:24:45 +0000 (15:24 +0000)]
removed spurious "

15 years agotentative subst-sexpand and change
Enrico Tassi [Mon, 30 Mar 2009 16:13:40 +0000 (16:13 +0000)]
tentative subst-sexpand and change

15 years ago...
Enrico Tassi [Mon, 30 Mar 2009 13:11:13 +0000 (13:11 +0000)]
...

15 years agomore comments
Enrico Tassi [Fri, 27 Mar 2009 12:12:50 +0000 (12:12 +0000)]
more comments

15 years agoexec and distribute implemented
Enrico Tassi [Fri, 27 Mar 2009 12:11:01 +0000 (12:11 +0000)]
exec and distribute implemented

15 years agonew apply almost there
Enrico Tassi [Thu, 26 Mar 2009 12:29:56 +0000 (12:29 +0000)]
new apply almost there

15 years ago...
Enrico Tassi [Thu, 26 Mar 2009 12:29:35 +0000 (12:29 +0000)]
...

15 years ago...
Enrico Tassi [Thu, 26 Mar 2009 12:29:28 +0000 (12:29 +0000)]
...

15 years agonew tactics are almost ready
Enrico Tassi [Wed, 25 Mar 2009 20:41:04 +0000 (20:41 +0000)]
new tactics are almost ready

15 years ago...
Claudio Sacerdoti Coen [Thu, 19 Mar 2009 22:01:12 +0000 (22:01 +0000)]
...

15 years agoadd Homepage field
Stefano Zacchiroli [Thu, 19 Mar 2009 10:13:36 +0000 (10:13 +0000)]
add Homepage field

15 years agoset package section to "ocaml"
Stefano Zacchiroli [Thu, 19 Mar 2009 10:10:18 +0000 (10:10 +0000)]
set package section to "ocaml"

15 years agoadd missing ${misc:Depends}, thanks lintian!
Stefano Zacchiroli [Thu, 19 Mar 2009 10:09:36 +0000 (10:09 +0000)]
add missing ${misc:Depends}, thanks lintian!

15 years agorelease to unstable
Stefano Zacchiroli [Thu, 19 Mar 2009 10:07:10 +0000 (10:07 +0000)]
release to unstable

15 years agodebian/*.in: more abstract substvars
Stefano Zacchiroli [Thu, 19 Mar 2009 10:05:15 +0000 (10:05 +0000)]
debian/*.in: more abstract substvars

15 years agodebian/rules: use ocaml.mk as a CDBS "rules" snippet
Stefano Zacchiroli [Thu, 19 Mar 2009 10:04:18 +0000 (10:04 +0000)]
debian/rules: use ocaml.mk as a CDBS "rules" snippet

15 years agorefresh build-dependencies for the transition
Stefano Zacchiroli [Thu, 19 Mar 2009 10:03:32 +0000 (10:03 +0000)]
refresh build-dependencies for the transition

15 years agoadded mactions, the three can now be collapsed to fit the screen
Enrico Tassi [Mon, 16 Mar 2009 12:55:03 +0000 (12:55 +0000)]
added mactions, the three can now be collapsed to fit the screen

15 years agoNew parameters for applyS: 10 20.
Andrea Asperti [Mon, 16 Mar 2009 12:41:36 +0000 (12:41 +0000)]
New parameters for applyS: 10 20.

15 years agoAdapted to new applyS.
Andrea Asperti [Mon, 16 Mar 2009 12:40:32 +0000 (12:40 +0000)]
Adapted to new applyS.

15 years agoAdded a property.
Andrea Asperti [Mon, 16 Mar 2009 12:39:54 +0000 (12:39 +0000)]
Added a property.

15 years agoMore details on the proof.
Claudio Sacerdoti Coen [Thu, 12 Mar 2009 09:37:27 +0000 (09:37 +0000)]
More details on the proof.

15 years agoNew algorithm based on in-place modification of the graph.
Claudio Sacerdoti Coen [Thu, 12 Mar 2009 00:08:54 +0000 (00:08 +0000)]
New algorithm based on in-place modification of the graph.
Conjecture solved in the negative:

(CMM?)+ | (MM?C)+

cCw = Cw
-Cw = MCw
cMw = CMw
-MMw = -w
-MCw = MMCw
iw = w

15 years agomatitacLib: Gc.compact added after the compilation of mmas
Ferruccio Guidi [Wed, 11 Mar 2009 18:39:42 +0000 (18:39 +0000)]
matitacLib: Gc.compact added after the compilation of mmas
            Now LAMBDA-TYPES compiles in ~ 100m
Makefile: daily test of LAMBDA-TYPES re-enabled

15 years agoProcedural: id tactics are not counted, ie they are placeholders
Ferruccio Guidi [Wed, 11 Mar 2009 15:37:54 +0000 (15:37 +0000)]
Procedural: id tactics are not counted, ie they are placeholders
LAMBDA-TYPES: bugfix in depend +
              makefile entries for %.ma %.mma %.ma.opt %.mma.opt

15 years agobug fix + better obj flavour guessing via inner sorts
Ferruccio Guidi [Wed, 11 Mar 2009 13:43:20 +0000 (13:43 +0000)]
bug fix + better obj flavour guessing via inner sorts

15 years agothe level 1 reconstruction procedure is now in Procedural1
Ferruccio Guidi [Wed, 11 Mar 2009 13:20:57 +0000 (13:20 +0000)]
the level 1 reconstruction procedure is now in Procedural1
Procedural2 coming soon ....

15 years ago....
Ferruccio Guidi [Wed, 11 Mar 2009 12:31:32 +0000 (12:31 +0000)]
....

15 years agonew dependences
Ferruccio Guidi [Wed, 11 Mar 2009 12:07:19 +0000 (12:07 +0000)]
new dependences

15 years agounification hints with recursive calls do work!
Enrico Tassi [Wed, 11 Mar 2009 09:48:31 +0000 (09:48 +0000)]
unification hints with recursive calls do work!

15 years agoadded margin option to the pp
Enrico Tassi [Wed, 11 Mar 2009 09:48:14 +0000 (09:48 +0000)]
added margin option to the pp

15 years agomore examples
Enrico Tassi [Wed, 11 Mar 2009 09:47:54 +0000 (09:47 +0000)]
more examples

15 years agounificatiom hints with premises
Enrico Tassi [Tue, 10 Mar 2009 21:07:46 +0000 (21:07 +0000)]
unificatiom hints with premises

15 years agoadded some commented debugging instructions :)
Ferruccio Guidi [Tue, 10 Mar 2009 20:16:58 +0000 (20:16 +0000)]
added some commented debugging instructions :)

15 years agounification hints almost ready
Enrico Tassi [Tue, 10 Mar 2009 17:51:12 +0000 (17:51 +0000)]
unification hints almost ready

15 years agonotation ++
Enrico Tassi [Tue, 10 Mar 2009 17:49:39 +0000 (17:49 +0000)]
notation ++

15 years agoA version of applyS with bounded iterations of given_clause (10+10).
Andrea Asperti [Tue, 10 Mar 2009 16:07:03 +0000 (16:07 +0000)]
A version of applyS with bounded iterations of given_clause (10+10).
Not sure it works on the full library.

15 years agoRemoved the context from the metasenv to avoid trivial typing errors (lists
Andrea Asperti [Tue, 10 Mar 2009 15:52:26 +0000 (15:52 +0000)]
Removed the context from the metasenv to avoid trivial typing errors (lists
with different lengths).

15 years ago...
Enrico Tassi [Mon, 9 Mar 2009 18:21:23 +0000 (18:21 +0000)]
...

15 years agoMinor improvements in pretty-printing.
Claudio Sacerdoti Coen [Fri, 6 Mar 2009 16:23:45 +0000 (16:23 +0000)]
Minor improvements in pretty-printing.

15 years agoNew version: only new nodes are normalized; moreover, reduction stops as soon
Claudio Sacerdoti Coen [Thu, 5 Mar 2009 11:47:13 +0000 (11:47 +0000)]
New version: only new nodes are normalized; moreover, reduction stops as soon
as the term becomes shorter.

15 years ago- fixed hint generation, more hints are generated
Enrico Tassi [Tue, 3 Mar 2009 20:16:35 +0000 (20:16 +0000)]
- fixed hint generation, more hints are generated
- fixpoint refinement added
- Appl [Meta _; ... ] handled correctly, no double Appl or Beta redex is
  generated (both in regular code and interators)

15 years ago...
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:37:33 +0000 (23:37 +0000)]
...

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:36:26 +0000 (23:36 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:36:13 +0000 (23:36 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:36:00 +0000 (23:36 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:46 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:31 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:16 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:02 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:34:46 +0000 (23:34 +0000)]
New version.

15 years agoFirst version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:34:30 +0000 (23:34 +0000)]
First version.

15 years agoOld algorithm moved to old to leave place to the new one.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:33:21 +0000 (23:33 +0000)]
Old algorithm moved to old to leave place to the new one.