haskell_inference
Ghazi Bouselmi's Pages
Here you can find out who I am. Well, also my CV, my publications
LinkedIn : http://www.linkedin.com/in/ghazibouselmi
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.
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>