]> matita.cs.unibo.it Git - fireball-separation.git/log
fireball-separation.git
6 years agoImproved backtracking in Simple
acondolu [Sun, 10 Jun 2018 14:38:56 +0000 (16:38 +0200)]
Improved backtracking in Simple

- Removed Fail exception, replaced by combination
  of Failure, Backtrack, Unseparable
- Added label to problem

6 years agoImplemented garbage in Num
acondolu [Sun, 10 Jun 2018 11:37:51 +0000 (13:37 +0200)]
Implemented garbage in Num

- Implemented parsing of garbage
  e.g. (x. x x , A , B , ...) where the garbage is A and B and ...
- Garbage is not implemented in Lambda4, but implemented in Num (except in subst i.e. reduction)
  (see `assert g = []`)
- Added sample problems with garbage

6 years agoFix: bug in printing garbage, did not consider the level
acondolu [Sun, 10 Jun 2018 11:22:20 +0000 (13:22 +0200)]
Fix: bug in printing garbage, did not consider the level

6 years agoAdded garbage to L
acondolu [Sat, 9 Jun 2018 08:27:14 +0000 (10:27 +0200)]
Added garbage to L

Note: eta_eq ignores garbage at the moment

6 years agoRemoved eat, p.stepped, p.phase and t.B
acondolu [Sat, 9 Jun 2018 08:19:56 +0000 (10:19 +0200)]
Removed eat, p.stepped, p.phase and t.B

6 years agoMore randomness in test generation
Claudio Sacerdoti Coen [Thu, 7 Jun 2018 17:43:58 +0000 (19:43 +0200)]
More randomness in test generation

6 years agoAdded problems that fail when eat is done incorrectly
acondolu [Thu, 7 Jun 2018 16:10:03 +0000 (18:10 +0200)]
Added problems that fail when eat is done incorrectly

i.e. on arguments before the max arity in the conv

6 years agoUsing andrea's finish instead of eat. All tests succeed.
acondolu [Thu, 7 Jun 2018 16:08:10 +0000 (18:08 +0200)]
Using andrea's finish instead of eat. All tests succeed.

But again, most generated tests are solved in one step.

6 years agoTrailing constant args in p.div are removed by sanity
acondolu [Thu, 7 Jun 2018 16:06:05 +0000 (18:06 +0200)]
Trailing constant args in p.div are removed by sanity

Because they cannot contribute to any usable eta-difference

6 years agoIt shows bug with new eat
Claudio Sacerdoti Coen [Thu, 7 Jun 2018 09:40:53 +0000 (11:40 +0200)]
It shows bug with new eat

6 years agoNew failing test
Claudio Sacerdoti Coen [Thu, 7 Jun 2018 09:19:49 +0000 (11:19 +0200)]
New failing test

6 years agoAdded tests with constants
acondolu [Thu, 7 Jun 2018 09:13:09 +0000 (11:13 +0200)]
Added tests with constants

- Enabled with flag --with-const
- Stores failing problems in problems/ folder

6 years agoProblems that are not distinct commented out.
Claudio Sacerdoti Coen [Wed, 6 Jun 2018 15:37:29 +0000 (17:37 +0200)]
Problems that are not distinct commented out.

Those problems can be separated, but picking a different
term to diverge

6 years agoFix: eating a lambda^n.C args is bad
Claudio Sacerdoti Coen [Wed, 6 Jun 2018 15:36:55 +0000 (17:36 +0200)]
Fix: eating a lambda^n.C args is bad

I know eat an argument which is a flexible inert.
What to do if there is none? I think we should backtrack;
for the time being I raise an assert false.

6 years agoAll output to stdout (in place of stderr).
Claudio Sacerdoti Coen [Wed, 6 Jun 2018 15:02:10 +0000 (17:02 +0200)]
All output to stdout (in place of stderr).

This commit could be cherry-picked in the other branches as well.

6 years agoFix: find_eta_difference now works with inerts of arbitrary length
Claudio Sacerdoti Coen [Wed, 6 Jun 2018 15:01:41 +0000 (17:01 +0200)]
Fix: find_eta_difference now works with inerts of arbitrary length

All simple.x tests now pass (same for automatically generated ones)

6 years agoForgot to commit yesterday file with problems with constants
acondolu [Sat, 2 Jun 2018 15:59:07 +0000 (17:59 +0200)]
Forgot to commit yesterday file with problems with constants

6 years agoExperimenting with backtracking and stepping on "all" possible subterms
acondolu [Fri, 1 Jun 2018 15:45:48 +0000 (17:45 +0200)]
Experimenting with backtracking and stepping on "all" possible subterms

6 years agoImplementing constants
acondolu [Fri, 1 Jun 2018 15:12:42 +0000 (17:12 +0200)]
Implementing constants

auto now iterates the eta differences and backtracks if no more available

6 years agoRemoved parameter from C
acondolu [Fri, 1 Jun 2018 14:17:19 +0000 (16:17 +0200)]
Removed parameter from C

6 years agoMore comments and improved find_eta_difference
acondolu [Fri, 1 Jun 2018 12:27:15 +0000 (14:27 +0200)]
More comments and improved find_eta_difference

6 years agoMore comments and better variable names
acondolu [Fri, 1 Jun 2018 08:18:20 +0000 (10:18 +0200)]
More comments and better variable names

6 years agoRenamed output files
acondolu [Fri, 1 Jun 2018 07:48:13 +0000 (09:48 +0200)]
Renamed output files

6 years agoRemoved warning
acondolu [Fri, 1 Jun 2018 07:44:18 +0000 (09:44 +0200)]
Removed warning

6 years agoFix lifting bug in unwind
Claudio Sacerdoti Coen [Thu, 31 May 2018 23:05:17 +0000 (01:05 +0200)]
Fix lifting bug in unwind

problems/simple.* now pass

6 years agoSimplified divergent problem
Claudio Sacerdoti Coen [Thu, 31 May 2018 22:34:45 +0000 (00:34 +0200)]
Simplified divergent problem

C diverges in pure

6 years agoMake the code OCaml-4.06.1-friendly
Claudio Sacerdoti Coen [Thu, 31 May 2018 21:45:14 +0000 (23:45 +0200)]
Make the code OCaml-4.06.1-friendly

6 years agoUpdated simple with current parser
acondolu [Thu, 31 May 2018 21:38:31 +0000 (23:38 +0200)]
Updated simple with current parser

- Removed parser_andrea
- Generalized problems.ml
- Moved sample problems from simple.ml to problems/simple.0

6 years agoSimpler tests in simple_test.ml + Added diverging tests in simple.1
acondolu [Thu, 31 May 2018 19:11:29 +0000 (21:11 +0200)]
Simpler tests in simple_test.ml + Added diverging tests in simple.1

6 years agoEat was erasing terms from C that made it diverge
acondolu [Thu, 31 May 2018 16:30:38 +0000 (18:30 +0200)]
Eat was erasing terms from C that made it diverge

6 years agoBug in mk_app with C
acondolu [Thu, 31 May 2018 16:29:52 +0000 (18:29 +0200)]
Bug in mk_app with C

6 years agoFix no_leading_lambdas to account for a step on x on an argument starting with x
acondolu [Thu, 31 May 2018 16:29:30 +0000 (18:29 +0200)]
Fix no_leading_lambdas to account for a step on x on an argument starting with x

6 years agoNew (in-)decision procedure for termination
acondolu [Thu, 31 May 2018 16:27:51 +0000 (18:27 +0200)]
New (in-)decision procedure for termination

6 years agoMore bound vars in simple_test
acondolu [Thu, 31 May 2018 13:48:06 +0000 (15:48 +0200)]
More bound vars in simple_test

6 years agoClean up, improve comments, move functions
acondolu [Thu, 31 May 2018 13:32:01 +0000 (15:32 +0200)]
Clean up, improve comments, move functions

`run' is the new entrypoint in simple.ml

6 years agoAdded check for eta_subterm in `solve'
acondolu [Thu, 31 May 2018 13:17:06 +0000 (15:17 +0200)]
Added check for eta_subterm in `solve'

Reverted sanity to old syntax

6 years agoAdded simple_test.ml
acondolu [Thu, 31 May 2018 12:55:57 +0000 (14:55 +0200)]
Added simple_test.ml

6 years agoMoved andrea.ml to simple.ml
acondolu [Thu, 31 May 2018 12:42:55 +0000 (14:42 +0200)]
Moved andrea.ml to simple.ml

6 years agoAdded constructor for constants
acondolu [Thu, 31 May 2018 12:40:38 +0000 (14:40 +0200)]
Added constructor for constants

TODO: correctly translate constants to pure terms in `purify'

6 years agoMade bombs more explosive (strongly)
acondolu [Wed, 30 May 2018 16:46:04 +0000 (18:46 +0200)]
Made bombs more explosive (strongly)

6 years agoRestored good check for Done
acondolu [Wed, 30 May 2018 16:06:14 +0000 (18:06 +0200)]
Restored good check for Done

6 years agoSimple strong separation implemented!
acondolu [Wed, 30 May 2018 14:31:24 +0000 (16:31 +0200)]
Simple strong separation implemented!

- Two phases for eat
- Moved code
- Reduction does not diverge (replaces DD with B)

6 years agoAdded check with purification to andrea.ml
acondolu [Wed, 30 May 2018 13:29:30 +0000 (15:29 +0200)]
Added check with purification to andrea.ml

Note! It now diverges because it uses B (bottoms)

6 years agoMoved function, fix indentation, removed parsing of bombs
acondolu [Wed, 30 May 2018 12:17:18 +0000 (14:17 +0200)]
Moved function, fix indentation, removed parsing of bombs

6 years agoClean-up step function; move code
acondolu [Wed, 30 May 2018 11:49:13 +0000 (13:49 +0200)]
Clean-up step function; move code

6 years agoRemoved pacman
acondolu [Wed, 30 May 2018 11:18:57 +0000 (13:18 +0200)]
Removed pacman

6 years agoClean up
acondolu [Wed, 30 May 2018 10:36:15 +0000 (12:36 +0200)]
Clean up

6 years agoget_subterm_with_head_and_args goes under lambdas
acondolu [Tue, 29 May 2018 09:03:53 +0000 (11:03 +0200)]
get_subterm_with_head_and_args goes under lambdas

6 years agoRemoved useless `isdiv' flag
acondolu [Tue, 29 May 2018 09:03:42 +0000 (11:03 +0200)]
Removed useless `isdiv' flag

6 years agoClean-up to examples. Removed tests.
acondolu [Tue, 29 May 2018 09:03:13 +0000 (11:03 +0200)]
Clean-up to examples. Removed tests.

6 years agoSimple algorithm by Andrea
acondolu [Wed, 30 May 2018 12:48:49 +0000 (14:48 +0200)]
Simple algorithm by Andrea

Cherry-picked from f260

6 years agoMoved env_of_sigma to Pure strong
acondolu [Wed, 30 May 2018 13:27:24 +0000 (15:27 +0200)]
Moved env_of_sigma to Pure

6 years agoTentative implementation of strong separation algorithm
acondolu [Mon, 28 May 2018 15:08:46 +0000 (17:08 +0200)]
Tentative implementation of strong separation algorithm

- A `Match from num is translated to pure by masking branches
  with underscore lambdas
- The eating step on the divergent does not create a substitution in sigma
  (to be understood...)
- In the branch of matches, \_. !divergent is translated to delta
- The checks in dangerous must still be fixed to go under lambdas

6 years agoMachine implements strong reduction
acondolu [Mon, 28 May 2018 13:14:34 +0000 (15:14 +0200)]
Machine implements strong reduction

The machine is very inefficient (uses unwind under lambdas)

6 years agoDetection of divergents master weak-reduction-separation
acondolu [Mon, 28 May 2018 13:03:00 +0000 (15:03 +0200)]
Detection of divergents

6 years agoBug fixed in pretty-printing of original names under lambdas
acondolu [Tue, 25 Jul 2017 14:57:26 +0000 (16:57 +0200)]
Bug fixed in pretty-printing of original names under lambdas

6 years agoFix in pretty-printing of match
acondolu [Tue, 25 Jul 2017 14:49:11 +0000 (16:49 +0200)]
Fix in pretty-printing of match

6 years agoImplemented parsing of "nominal" variables (`@`)
acondolu [Tue, 25 Jul 2017 08:21:16 +0000 (10:21 +0200)]
Implemented parsing of "nominal" variables (`@`)

Each occurrence of `@` is parsed as a fresh free variable

6 years agoAllow comments (#) at the end of terms
acondolu [Mon, 24 Jul 2017 14:15:53 +0000 (16:15 +0200)]
Allow comments (#) at the end of terms

6 years agoLogging options to display measure of single terms in string_of_problem
acondolu [Mon, 24 Jul 2017 14:15:19 +0000 (16:15 +0200)]
Logging options to display measure of single terms in string_of_problem

6 years agoFixed bug in computing special k
acondolu [Mon, 24 Jul 2017 12:55:31 +0000 (14:55 +0200)]
Fixed bug in computing special k

6 years agoRemoved special strategies in choose_step
acondolu [Mon, 24 Jul 2017 12:05:08 +0000 (14:05 +0200)]
Removed special strategies in choose_step

6 years agoBetter error messages in parser
acondolu [Sun, 23 Jul 2017 20:23:34 +0000 (22:23 +0200)]
Better error messages in parser

(cherry picked from commit 54e55518261ee5f3c68758ea070b1bac41400e54)

6 years agoRevert subst in branches of matches
acondolu [Sun, 23 Jul 2017 07:59:00 +0000 (09:59 +0200)]
Revert subst in branches of matches

Actually, it could be moved in susbt_in_problem,
hence doing it only once (on the deltas), instead
of replacing multiple times like now (useless).

(cherry picked from commit bd3a8ee424e495ab4003f6d4cb88579f29e3bc3a)

6 years agoComments, fix indentation and
acondolu [Sat, 22 Jul 2017 20:35:44 +0000 (22:35 +0200)]
Comments, fix indentation and

(cherry picked from commit 0a50c398d9eef65620f18f99ef675770b50a920c)

6 years agoRenamed in critical_showstoppers: showstoppers -> inedible (I don't know why)
acondolu [Sat, 22 Jul 2017 19:58:31 +0000 (21:58 +0200)]
Renamed in critical_showstoppers: showstoppers -> inedible (I don't know why)

(cherry picked from commit dc829653c03f7bf0977addabe480e7c8b178bad1)

6 years agoSimplified arity_of, precompute_edible_data, critical_showsteppers
acondolu [Sat, 22 Jul 2017 19:34:23 +0000 (21:34 +0200)]
Simplified arity_of, precompute_edible_data, critical_showsteppers

(cherry picked from commit 4c81587c5f911c4d5f818765106bb5373967d715)

6 years agoAdded a couple of tests which MUST fail
acondolu [Fri, 25 May 2018 15:03:18 +0000 (17:03 +0200)]
Added a couple of tests which MUST fail

6 years agoFixed computation of arity for top-level inerts
acondolu [Sat, 22 Jul 2017 19:00:26 +0000 (21:00 +0200)]
Fixed computation of arity for top-level inerts

(cherry picked from commit 5682bf463b89edb7756020fe7b838eb846d6c771)

6 years agoSimplified not-working example
acondolu [Sat, 22 Jul 2017 18:59:55 +0000 (20:59 +0200)]
Simplified not-working example

(cherry picked from commit 180710db0f9d6f81edd7a5cc1bfce41e3b3e620a)

6 years agoMissing parenthesis fixed
Claudio Sacerdoti Coen [Tue, 18 Jul 2017 15:55:29 +0000 (17:55 +0200)]
Missing parenthesis fixed

(cherry picked from commit aa18ab71f3030f746de14168b9dae21c255e9b81)

6 years agoFailing case found
Claudio Sacerdoti Coen [Tue, 18 Jul 2017 13:38:27 +0000 (15:38 +0200)]
Failing case found

(cherry picked from commit 42eb14bc4443ce5a9bb893654db97a9c41486f06)

6 years agoHack to reserve var 0 to purify it to BOM removed
Claudio Sacerdoti Coen [Tue, 18 Jul 2017 13:36:56 +0000 (15:36 +0200)]
Hack to reserve var 0 to purify it to BOM removed

(cherry picked from commit 1fdb461d0bc4056ade8a05c482142984dbda735c)

6 years agosubst does not replace anymore in branches of maches
acondolu [Sun, 16 Jul 2017 14:01:21 +0000 (16:01 +0200)]
subst does not replace anymore in branches of maches

It was unnecessary: a match cannot expand to a previous branch

(cherry picked from commit 8a90160900bb95133b8e204a4fcadaa2db2f11dd)

6 years agoPrinting now preserves the names of the original free variables
acondolu [Sun, 16 Jul 2017 13:41:16 +0000 (15:41 +0200)]
Printing now preserves the names of the original free variables

(cherry picked from commit 7051416c234181eaf79dedfd18005cdf0a3e0863)

6 years agoImproved parsing
acondolu [Sat, 15 Jul 2017 18:23:20 +0000 (20:23 +0200)]
Improved parsing

- removed unused parse'
- fixed bug which was ignoring the first problems in some files

(cherry picked from commit 2d56686ea25883e77d0a69f1245e6e840fc8be5f)

6 years agoImproved pretty-printing
acondolu [Sat, 15 Jul 2017 18:21:39 +0000 (20:21 +0200)]
Improved pretty-printing

- Num does not use print_name anymore
- Original names of free variables are preserved
- bound variables' names start with x

(cherry picked from commit 137e2373f8875992898f8be0e07c4299ffbf3516)

6 years agoAdded problem wrongly backtracking
acondolu [Sat, 15 Jul 2017 15:16:51 +0000 (17:16 +0200)]
Added problem wrongly backtracking

(cherry picked from commit a34071ed728b8de44b198de4e73a52207557ed81)

6 years agoForgot one "Z"
acondolu [Sat, 15 Jul 2017 15:00:04 +0000 (17:00 +0200)]
Forgot one "Z"

(cherry picked from commit 572c25c8db51bd571c7f4810500074bac8c37c31)

6 years agoCode clean-up
acondolu [Sat, 15 Jul 2017 14:47:50 +0000 (16:47 +0200)]
Code clean-up

(cherry picked from commit 8fcb433208ce608350ea554dd1d92fa5a45fd463)

6 years agoCode clean-up
acondolu [Sat, 15 Jul 2017 14:41:53 +0000 (16:41 +0200)]
Code clean-up

(cherry picked from commit 5d8249a042beefbe21bfeed48619ed1917ebbcb7)

6 years agoImportant: added special variable "Z" for zero.
acondolu [Sat, 15 Jul 2017 14:41:39 +0000 (16:41 +0200)]
Important: added special variable "Z" for zero.

- Removed append_zero in Lambda4
- Now tests append "Z" at the end of ps'
- Manually appended "Z" at the end of all problems
- Removed tmp function in Lambda4, renamed to problem_of

(cherry picked from commit 82dd1911598932af386c4de46398624453e1fc31)

6 years agoMoved all problems in problems folder. Last ones in "w"
acondolu [Sat, 15 Jul 2017 14:01:36 +0000 (16:01 +0200)]
Moved all problems in problems folder. Last ones in "w"

(cherry picked from commit f7a60345135a4032bf63a7dc650bcc9fe30aa30a)

6 years agoFixes to parser
acondolu [Sat, 15 Jul 2017 13:31:04 +0000 (15:31 +0200)]
Fixes to parser

(cherry picked from commit 666a228779e465d08a0deea2e35c0cccf5722b40)

6 years agoFixed "$" in parser
acondolu [Sat, 15 Jul 2017 13:05:34 +0000 (15:05 +0200)]
Fixed "$" in parser

(cherry picked from commit db562ac015ffc6c1a08c226b4eef7790b21661cd)

6 years agoCommand line arguments to ./a.out
acondolu [Fri, 14 Jul 2017 18:34:02 +0000 (20:34 +0200)]
Command line arguments to ./a.out

For example:
 ./a.out problems/*
 ./a.out problems/p

Moved "o"-problems to problems/o

(cherry picked from commit dfad242808c3525a0d9e3420565551964fcf0832)

6 years agoFixed problems separator in parser: now it is $
acondolu [Fri, 14 Jul 2017 18:32:20 +0000 (20:32 +0200)]
Fixed problems separator in parser: now it is $

A separable problem's label may start with '!', a not separable's with '?'

(cherry picked from commit 71f8eb7befd85ff4911658136597b41ed177ff8c)

6 years agoAdded label to problem
acondolu [Fri, 14 Jul 2017 18:30:55 +0000 (20:30 +0200)]
Added label to problem

(cherry picked from commit c7e39970b94c93db45f2629af3fdb1e08371eca1)

6 years agoFailure in case of empty problem, to be fixed
acondolu [Fri, 14 Jul 2017 17:39:21 +0000 (19:39 +0200)]
Failure in case of empty problem, to be fixed

(cherry picked from commit 605ae9159149e42a17f044bbfad94f7dc2de79c2)

6 years agoParser.from_file, and p* problems moved to problems/p
acondolu [Fri, 14 Jul 2017 17:28:29 +0000 (19:28 +0200)]
Parser.from_file, and p* problems moved to problems/p

(cherry picked from commit 032edbca0cd6654adae5b5f06620723e74847435)

6 years agoproblems now contain a label and the names of the original free variables
acondolu [Fri, 14 Jul 2017 17:25:23 +0000 (19:25 +0200)]
problems now contain a label and the names of the original free variables

(cherry picked from commit 15c305b0d106b39616bdeea9aec9febc7539c2c1)

6 years agoFirst draft of Parser.problem_of_string
acondolu [Fri, 14 Jul 2017 16:02:19 +0000 (18:02 +0200)]
First draft of Parser.problem_of_string

- problem_of_string should unify old Lambda4.problem_of and Parser.parse'
- Lambda4.problem_of was temporarily factored in problem_of_2
  and problem_of_String_tmp

(cherry picked from commit 8b69a4c59242b64294c7065a4e85437ce3cbc32d)

6 years agoChanged logic of entrypoint in Lambda4
acondolu [Fri, 14 Jul 2017 15:20:42 +0000 (17:20 +0200)]
Changed logic of entrypoint in Lambda4

- removed exception Fail
- added "check",which checks if we are in a subproblem
  of separation on which we know to be complete
- "solve" does not raise particular exceptions anymore,
  and the program raise failure only if there is some bug

(cherry picked from commit 608c40045f651c6402b17c437f997de4d63f6afd)

6 years agoMoved parse' from Num to Parser
acondolu [Fri, 14 Jul 2017 14:44:15 +0000 (16:44 +0200)]
Moved parse' from Num to Parser

(cherry picked from commit 123d64bb5ae7127f6a51cbf44b63341de001a187)

6 years agoFixed: was using compare in place of eta_eq
acondolu [Fri, 14 Jul 2017 12:39:10 +0000 (14:39 +0200)]
Fixed: was using compare in place of eta_eq

in particular, eta_eq ignores arities of variables

there used to be cases of duplicate entries in PS (up to arities of variables)

(cherry picked from commit 79e9bd64d15490dd5abc353cc5b09378d3c640d1)

6 years agoRe-use Util.index_of
acondolu [Fri, 14 Jul 2017 12:38:08 +0000 (14:38 +0200)]
Re-use Util.index_of

(cherry picked from commit 52947a60467ebb10cec57ffc1725644ad605c671)

6 years agoCode clean-up
acondolu [Fri, 14 Jul 2017 12:31:30 +0000 (14:31 +0200)]
Code clean-up

Less casts and casts in the right place

(cherry picked from commit 6bf723ba426a04a3ae5d36baf8a9fe4bffebc635)

6 years agoTidying up problems.ml
acondolu [Fri, 14 Jul 2017 08:57:22 +0000 (10:57 +0200)]
Tidying up problems.ml

(cherry picked from commit c8d9c2fda6b135b29e81e3bea95520ba449b86e3)

6 years agoTentative commit: tactics dropped and clean-up
acondolu [Thu, 13 Jul 2017 15:38:23 +0000 (17:38 +0200)]
Tentative commit: tactics dropped and clean-up

(cherry picked from commit 0991fc5486c3158fc361e84cbba5aefa67893ba4)

Include codice di pure.ml che implementa Pure.B da commit
 "Removed bomb variable"

6 years agoAdded assert false
acondolu [Thu, 13 Jul 2017 18:35:37 +0000 (20:35 +0200)]
Added assert false

(cherry picked from commit ba6f0ecd9531b266361674d76423c24381dc72ee)