prove_evaluator.rb revision 63499d8d12a219d26744bcb896789ea28459814f
c25356d5978632df6203437e1953bcb29e0c736fTimo Sirainenmodule Hets
c25356d5978632df6203437e1953bcb29e0c736fTimo Sirainen module Prove
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen class ProveEvaluator < BaseEvaluator
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen include ProveEvaluationHelper
1299f2c3723ca9ccf8f9e563ec23ee1a1721fe4cTimo Sirainen
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen attr_accessor :proof_attempt
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen attr_accessor :object_hash, :hierarchy
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen register :all, :start, to: :all_start
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen register :all, :end, to: :all_end
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen
fd7ca4bdc1fb63547d997b6ddd639284cb5a0d01Timo Sirainen register :set_object_value, :start, to: :set_object_value
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen register :add_array_value, :start, to: :add_array_value
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen register :node, :start, to: :node_start
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen register :node, :end, to: :node_end
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen register :goal, :start, to: :goal_start
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen register :goal, :end, to: :goal_end
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen register :tactic_script, :start, to: :tactic_script_start
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen register :tactic_script, :end, to: :tactic_script_end
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen register :tactic_script_extra_options, :start,
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen to: :tactic_script_extra_options_start
8eea67470c1bd8562a62e7445d930bb2079b1a43Timo Sirainen register :tactic_script_extra_options, :end,
8eea67470c1bd8562a62e7445d930bb2079b1a43Timo Sirainen to: :tactic_script_extra_options_end
8eea67470c1bd8562a62e7445d930bb2079b1a43Timo Sirainen
8eea67470c1bd8562a62e7445d930bb2079b1a43Timo Sirainen register :used_prover, :start, to: :used_prover_start
8eea67470c1bd8562a62e7445d930bb2079b1a43Timo Sirainen register :used_prover, :end, to: :used_prover_end
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen register :used_time, :start, to: :used_time_start
87cc5e9025e7fb6408f0de64c48d2d2897773ba5Timo Sirainen register :used_time, :end, to: :used_time_end
939451389b8e0ad529277b84fe51dab38a8cf77cTimo Sirainen
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen register :used_time_components, :start, to: :used_time_components_start
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen register :used_time_components, :end, to: :used_time_components_end
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen
9c3577aeb78a27920439ad9f1e62ee03699378c3Timo Sirainen register :used_axioms, :start, to: :used_axioms_start
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen register :used_axioms, :end, to: :used_axioms_end
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen def initialize(*args, proof_attempt)
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen super(*args)
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen self.proof_attempt = proof_attempt
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen end
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen def all_start
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen self.hierarchy = []
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen end
6ef7e31619edfaa17ed044b45861d106a86191efTimo Sirainen
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen def all_end
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen end
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen def set_object_value(value, key)
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen info = proof_attempt_info(key, value)
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen object_hash[info.keys.first] = info.values.first if info
18ddd4fba186b1b407cae98bb388fa8add7db48dTimo Sirainen end
90ed03ab289947f5576d2c616ada27724f50e9cdTimo Sirainen
63b70dd3e4b4d68a02b1bf7d78e92076210e3e1aTimo Sirainen def add_array_value(value)
6ef7e31619edfaa17ed044b45861d106a86191efTimo Sirainen info = proof_attempt_info
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen object_hash[info.keys.first] ||= []
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen object_hash[info.keys.first] << value
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen end
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen def node_start
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen hierarchy << :node
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen self.object_hash = {}
d1414c09cf0d58ac983054e2f4e1a1f329272dcfTimo Sirainen end
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen def node_end
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen hierarchy.pop
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen end
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen
8eea67470c1bd8562a62e7445d930bb2079b1a43Timo Sirainen def goal_start
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen hierarchy << :goal
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen ontology_name = object_hash[:ontology_name]
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen self.object_hash = {ontology_name: ontology_name}
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen end
64e244defe74f513ce94f33d000a048ddbe2ea23Timo Sirainen
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen def goal_end
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen hierarchy.pop
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen fill_proof_attempt_from_hash(object_hash)
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen end
73bfdbe28c2ce6d143eadf0bab8ccfbe4cab0faeTimo Sirainen
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen %i(tactic_script
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen tactic_script_extra_options
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen used_prover
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen used_time
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen used_time_components
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen used_axioms).each do |hook|
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen define_method("#{hook}_start") do
66c3f635f2f33905af527d49b27f95322aa7dfa7Timo Sirainen hierarchy << hook
66c3f635f2f33905af527d49b27f95322aa7dfa7Timo Sirainen end
acf3b7bf3a8891b118a71c45e6c48d17bc90b259Timo Sirainen
2a90d8a14b0e7cc1508814bc87d3dfa598ef46a8Timo Sirainen define_method("#{hook}_end") do
hierarchy.pop
end
end
def proof_attempt_info(key = nil, value = nil)
case hierarchy.last
when :node
{ontology_name: value} if key == 'node'
when :goal
goal_info(key, value)
when :tactic_script
{:"tactic_script_#{key.underscore}" => value}
when :tactic_script_extra_options
{:tactic_script_extra_options => nil}
when :used_prover
{:"used_prover_#{key.underscore}" => value}
when :used_time
{:time_taken => value} if key == 'seconds'
when :used_time_components
# don't use them
when :used_axioms
{:used_axioms => nil}
else
{key.underscore.to_sym => value}
end
end
def goal_info(key, value)
if key == 'name'
{:theorem_name => value}
else
{key.underscore.to_sym => value}
end
end
end
end
end