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

7 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

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

7 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

7 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.

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

7 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

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

7 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

7 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

7 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

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

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

7 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

7 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

7 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

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