haskell_inference2

The challenge definition can be found here "Elementary Wattson". The code is again a bit too dense, it had to be compressed to fit in the maximum 50KB allowed by HakerRank.

19-06-2017 : first draft : grammar definition and input tokenization.

21-06-2017 : bug fixes, first matching/substitution functions, manual proving tests.

23-06-2017 : bug fixes, matching/substitution functions.

26-06-2017 : bug fixes, first success on reccursive proving on some simple cases: still not fully operational.

26-06-2017_bis : bug fixes, fix for infinite inference loops; 20% success rate.

27-06-2017 : nasty bug fix: error in merging lists of constraints/variables instantiation; 40% success rate ( 80% if ignoring the sorting of the results).

=> TODO: proper handling of equality assertions while proving in premises.

The next attempts are aimed at handling equality assertions prior to the proving procedure, as well as solving out-of-memory errors & dead loops.

02-07-2017

04-07-2017

05-07-2017

06-07-2017

07-07-2017

The grammar:

<operation> ::= <rule> | <query> | <command> | <no-op>

<no-op> ::= <NOTHING>

| "%" <comment>

<command> ::= "quit" "!"

<query> ::= "(" <complex-term-list> ")" "?"

<rule> ::= <simple-term> "."

| "{" "(" <complex-term-list> ")" "=>" <simple-term> "}" "."

<complex-term-list> ::= <complex-term>

| <complex-term> "," <complex-terms-list>

<complex-term> ::= <simple-term>

| <equality-assert>

<equality-assert> ::= "<" <simple-term> ["=" | "/="]<simple-term> ">"

<simple-term> ::= <name>

| <var>

| <relational-term>

<var> ::= "#" <number> <var> -- this is used internally for var renaming

| "#" <name>

<relational-term> ::= "[" <name> ":" <simple-term-list> "]"

<simple-term-list> ::= <simple-term>

| <simple-term> "," <simple-term-list>