]> matita.cs.unibo.it Git - helm.git/log
helm.git
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.

15 years agocicInspect: node count fixed
Ferruccio Guidi [Mon, 2 Mar 2009 20:34:04 +0000 (20:34 +0000)]
cicInspect: node count fixed
proceduralTeX: bug fix
LAMBDA-TYPES/Legacy-2/preamble.ma: bug fix
character: updated

15 years agouri renaming and new nodes count
Ferruccio Guidi [Mon, 2 Mar 2009 12:39:33 +0000 (12:39 +0000)]
uri renaming and new nodes count

15 years agosome renaming to comply with new naming policy ...
Ferruccio Guidi [Mon, 2 Mar 2009 12:03:37 +0000 (12:03 +0000)]
some renaming to comply with new naming policy ...

15 years agocicInspect: now we can choose not to count the Cic.Implicit constructors
Ferruccio Guidi [Thu, 26 Feb 2009 21:15:13 +0000 (21:15 +0000)]
cicInspect: now we can choose not to count the Cic.Implicit constructors
proceduralTypes, proceduralOptimizer: we do not count the Cic.Implict nodes
proceduralTeX: bug fix

15 years agoProceduralTeX completed and tested on the terms given as examples in the paper about...
Ferruccio Guidi [Wed, 25 Feb 2009 20:54:13 +0000 (20:54 +0000)]
ProceduralTeX completed and tested on the terms given as examples in the paper about the procedural reconstruction

15 years ago...
Enrico Tassi [Wed, 25 Feb 2009 09:11:26 +0000 (09:11 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 24 Feb 2009 15:23:38 +0000 (15:23 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 24 Feb 2009 15:19:41 +0000 (15:19 +0000)]
...

15 years agoNew module for TeX rendering of procedural input/output
Ferruccio Guidi [Sat, 21 Feb 2009 22:19:18 +0000 (22:19 +0000)]
New module for TeX rendering of procedural input/output
Used in the papers about the procedural representation

15 years ago...
Enrico Tassi [Fri, 20 Feb 2009 10:08:20 +0000 (10:08 +0000)]
...

15 years ago...
Enrico Tassi [Fri, 20 Feb 2009 09:22:21 +0000 (09:22 +0000)]
...

15 years ago- Coq/preamble: missing alias added
Ferruccio Guidi [Tue, 17 Feb 2009 19:37:22 +0000 (19:37 +0000)]
- Coq/preamble: missing alias added
- nUri: head comment fixed
- Procedural: the cases tactic is now detected and generated
              but does not compile :))
- grafiteAstPp: output syntax of the cases tactic fixed
- grafiteParser: impovement in the code for the elim tactic

15 years agosome notational experiments
Enrico Tassi [Mon, 16 Feb 2009 16:27:36 +0000 (16:27 +0000)]
some notational experiments

15 years ago...
Enrico Tassi [Sun, 15 Feb 2009 19:46:21 +0000 (19:46 +0000)]
...

15 years ago...
Enrico Tassi [Sun, 15 Feb 2009 15:19:09 +0000 (15:19 +0000)]
...

15 years ago...
Enrico Tassi [Sun, 15 Feb 2009 14:58:52 +0000 (14:58 +0000)]
...

15 years agocommented some printings
Enrico Tassi [Sun, 15 Feb 2009 14:57:16 +0000 (14:57 +0000)]
commented some printings

15 years agominor changes to make the library compile after wilmers new exists.
Enrico Tassi [Sun, 15 Feb 2009 14:56:26 +0000 (14:56 +0000)]
minor changes to make the library compile after wilmers new exists.

15 years agoAxiomatization of real numbers (work in progress)
Wilmer Ricciotti [Fri, 13 Feb 2009 15:16:55 +0000 (15:16 +0000)]
Axiomatization of real numbers (work in progress)