]> matita.cs.unibo.it Git - fireball-separation.git/log
fireball-separation.git
6 years agoRemove FORCE option in Makefile
acondolu [Thu, 13 Jul 2017 18:34:50 +0000 (20:34 +0200)]
Remove FORCE option in Makefile

(cherry picked from commit 6ba14f58fa4c8f93fc2a398bdee030cd2217adea)

6 years agoFix: missing check to avoid stepping on vars of non positive arity
acondolu [Thu, 13 Jul 2017 17:05:39 +0000 (19:05 +0200)]
Fix: missing check to avoid stepping on vars of non positive arity

(cherry picked from commit 58f1518398346a81ccd8d0b14a14565b8bff5276)

6 years agoFix: max_arity_tms was using wrong comparison
acondolu [Thu, 13 Jul 2017 15:34:12 +0000 (17:34 +0200)]
Fix: max_arity_tms was using wrong comparison

(cherry picked from commit a104858f2dd754e5d086c3884823f3f39d716691)

6 years agoAdded variable convergent_dummy
acondolu [Mon, 28 May 2018 08:56:07 +0000 (10:56 +0200)]
Added variable convergent_dummy

6 years agoFixes to printing
acondolu [Wed, 12 Jul 2017 21:28:46 +0000 (23:28 +0200)]
Fixes to printing

(cherry picked from commit 4627d2b89b5a96e09b1921e033a5c1d7dd50dbc6)

6 years agoDisabled some chars as variable names in the parser
acondolu [Wed, 12 Jul 2017 21:12:44 +0000 (23:12 +0200)]
Disabled some chars as variable names in the parser

(cherry picked from commit bfd8f8a98a7392ac8cbd9070a8e4ff4d06e09510)

6 years agoPrettier-printing: string_of_problem outputs OCaml code
acondolu [Wed, 12 Jul 2017 19:48:01 +0000 (21:48 +0200)]
Prettier-printing: string_of_problem outputs OCaml code

(cherry picked from commit d97b1a852472085bf3449e34f3b25aee349686fd)

6 years agoFixed if-then-else
acondolu [Tue, 11 Jul 2017 15:40:00 +0000 (17:40 +0200)]
Fixed if-then-else

(cherry picked from commit 588a00cd5ae861a2f366df992f758f285265a34a)

6 years agoFix: nested `Lambda(false,_) were not handled correctly
acondolu [Tue, 11 Jul 2017 15:39:37 +0000 (17:39 +0200)]
Fix: nested `Lambda(false,_) were not handled correctly

(cherry picked from commit 0147bacbe2db4055ae6f991aaa64a9fb1047edc6)

6 years ago-666 -> min_int
acondolu [Tue, 11 Jul 2017 15:38:14 +0000 (17:38 +0200)]
-666 -> min_int

(cherry picked from commit 5da7cf1322998c8965455264249f12ac4400f49d)

6 years agoFixed indentation and logging
acondolu [Tue, 11 Jul 2017 14:38:26 +0000 (16:38 +0200)]
Fixed indentation and logging

(cherry picked from commit 4985769db038aa060b47ab40f673aaaacea54742)

6 years agoclean removes *.o files
acondolu [Tue, 11 Jul 2017 13:44:40 +0000 (15:44 +0200)]
clean removes *.o files

6 years agoRemoved old .ar files
acondolu [Tue, 11 Jul 2017 13:44:16 +0000 (15:44 +0200)]
Removed old .ar files

6 years agoRun tests with: make run
acondolu [Tue, 11 Jul 2017 13:42:09 +0000 (15:42 +0200)]
Run tests with: make run

6 years agoFix: conv : x:min_int (.... y:1 ...) y was not considered for stepping
acondolu [Tue, 11 Jul 2017 12:00:34 +0000 (14:00 +0200)]
Fix: conv : x:min_int (.... y:1 ...)  y was not considered for stepping

When no other choice is available, step on any >0 variable that occurs in
a conv.

6 years agoNew problems n1, n2 used to debug the problem with dangerous variables fixed in the...
acondolu [Tue, 11 Jul 2017 11:24:09 +0000 (13:24 +0200)]
New problems n1, n2 used to debug the problem with dangerous variables fixed in the last commits

6 years agoBug fix: x (y z) where y was conv_dangerous did not make x so
acondolu [Tue, 11 Jul 2017 11:22:41 +0000 (13:22 +0200)]
Bug fix: x (y z) where y was conv_dangerous did not make x so

Additional fix to last commit: args' where no longer checked for dangerous
variables. Fixed by passing three arguments to dangerous_invert_conv in
place of two.

6 years agoFix bug in dangerous_conv with arity of arguments of matches.
acondolu [Tue, 11 Jul 2017 09:37:18 +0000 (11:37 +0200)]
Fix bug in dangerous_conv with arity of arguments of matches.
Next bug: variable replaced twice

6 years agoThe measure finally works on all problems in problems.ml!
acondolu [Mon, 10 Jul 2017 16:44:31 +0000 (18:44 +0200)]
The measure finally works on all problems in problems.ml!
Added in logs/fail.txt a fragment of a failing problem

6 years agoExperimenting with a combined measure
acondolu [Mon, 10 Jul 2017 13:48:25 +0000 (15:48 +0200)]
Experimenting with a combined measure

6 years agoInstantiate now uses a global initialSpecialK (ignoring the local one)
acondolu [Mon, 10 Jul 2017 12:43:43 +0000 (14:43 +0200)]
Instantiate now uses a global initialSpecialK (ignoring the local one)
This fixes the bug in the previous commit, and makes the problem pass

6 years agoArity inherited only in the case (true, min_int)
acondolu [Mon, 10 Jul 2017 12:13:36 +0000 (14:13 +0200)]
Arity inherited only in the case (true, min_int)
Problem 25 fails because a fake variable becomes
critical step.

6 years agonew_arity = old_arity + 1
acondolu [Mon, 10 Jul 2017 12:06:55 +0000 (14:06 +0200)]
new_arity = old_arity + 1

6 years agoFixes to how arities are assigned and propagated
acondolu [Fri, 7 Jul 2017 17:16:29 +0000 (19:16 +0200)]
Fixes to how arities are assigned and propagated
- added truelam to subst (useless, can be removed)
- TODO: to measure the problem, count the `fake` variables
        which are the ones with arity = min_int

6 years agoMinor fixes
acondolu [Wed, 28 Jun 2017 14:29:21 +0000 (16:29 +0200)]
Minor fixes

6 years agostill stepping on negative variables
<andrea.condoluci@unibo.it> [Tue, 27 Jun 2017 13:16:43 +0000 (15:16 +0200)]
still stepping on negative variables

6 years agoProblems pass, but still missing computation of arities of fresh applicative vars
<andrea.condoluci@unibo.it> [Mon, 26 Jun 2017 11:47:30 +0000 (13:47 +0200)]
Problems pass, but still missing computation of arities of fresh applicative vars

6 years agoNew representation of arities in variables
<andrea.condoluci@unibo.it> [Mon, 26 Jun 2017 10:26:43 +0000 (12:26 +0200)]
New representation of arities in variables

6 years agoRemoved traces of lambda3
<andrea.condoluci@unibo.it> [Mon, 26 Jun 2017 09:37:07 +0000 (11:37 +0200)]
Removed traces of lambda3

6 years agoRemoved lambda3 + Fixed lambda4
<andrea.condoluci@unibo.it> [Thu, 22 Jun 2017 15:20:55 +0000 (17:20 +0200)]
Removed lambda3 + Fixed lambda4

6 years agoUpdated type of terms with arities in lambda and matche
<andrea.condoluci@unibo.it> [Thu, 22 Jun 2017 14:23:21 +0000 (16:23 +0200)]
Updated type of terms with arities in lambda and matche

6 years agoMoved andrea's stuff to its branch
<andrea.condoluci@unibo.it> [Mon, 12 Jun 2017 20:44:12 +0000 (22:44 +0200)]
Moved andrea's stuff to its branch

6 years agoCopy ocaml folder from sacerdot's svn repository, rev 4907
<andrea.condoluci@unibo.it> [Mon, 12 Jun 2017 20:28:38 +0000 (22:28 +0200)]
Copy ocaml folder from sacerdot's svn repository, rev 4907

6 years agoInitial commit
Andrea Condoluci [Mon, 12 Jun 2017 20:17:57 +0000 (22:17 +0200)]
Initial commit