Skip to content

Instantly share code, notes, and snippets.

@eagletmt

eagletmt/ideslave.rb

Last active December 16, 2015 22:29
Show Gist options
  • Save eagletmt/5507319 to your computer and use it in GitHub Desktop.
Save eagletmt/5507319 to your computer and use it in GitHub Desktop.
Download ZIP
coqtop -ideslave
Raw
ideslave.rb
#!/usr/bin/env ruby
require 'nokogiri'
module FromXml
class MappingError < StandardError
attr_reader :node
def initialize(node, msg = nil)
super msg
@node = node
end
end
class Failure < StandardError
attr_reader :loc_s, :loc_e
def initialize(node)
super node.inner_text
@loc_s = node['loc_s']
@loc_e = node['loc_e']
end
end
module_function
def convert(node)
case node['val']
when 'good'
of_value node.child
when 'fail'
raise Failure.new(node)
else
raise MappingError.new(node, 'Invalid toplevel value')
end
end
def of_value(node)
sym = "of_#{node.name}".to_sym
if respond_to? sym
send sym, node
else
raise MappingError.new(node, 'Unknown node type')
end
end
def of_list(node)
node.children.map do |child|
of_value child
end
end
def of_pair(node)
[of_value(node.children[0]), of_value(node.children[1])]
end
def of_unit(node)
nil
end
def of_string(node)
node.inner_text
end
def of_int(node)
node.inner_text.to_i
end
def of_bool(node)
case node['val']
when 'true'
true
when 'false'
false
else
raise MappingError.new(node, 'Invalid bool value')
end
end
def of_option(node)
case node['val']
when 'none'
nil
when 'some'
of_value node.child
else
raise MappingError.new(node, 'Invalid option value')
end
end
def of_option_state(node)
opt = {}
[:sync, :depr, :name, :value].each.with_index do |name, i|
if node.children[i].nil?
binding.pry
end
opt[name] = of_value node.children[i]
end
opt
end
def of_option_value(node)
child = node.child
case node['val']
when 'boolvalue'
of_bool child
when 'intvalue'
of_option child
when 'stringvalue'
of_string child
else
raise MappingError.new(node, 'Invalid option_value value')
end
end
def of_coq_info(node)
info = {}
[:version, :protocol, :release, :compile].each.with_index do |name, i|
info[name] = of_value node.children[i]
end
info
end
def of_status(node)
status = {}
[:path, :proofname, :allproofs, :statenum, :proofnum].each.with_index do |name, i|
status[name] = of_value node.children[i]
end
status
end
def of_goals(node)
goals = {}
[:fg, :bg].each.with_index do |name, i|
goals[name] = of_value node.children[i]
end
goals
end
def of_goal(node)
goal = {}
[:id, :hyp, :ccl].each.with_index do |name, i|
goal[name] = of_value node.children[i]
end
goal
end
def of_evar(node)
node.inner_text
end
# 8.4pl1: coq_object
# 8.4pl2: search_answer
def of_search_answer(node)
obj = {}
[:prefix, :qualid, :object].each.with_index do |name, i|
obj[name] = of_value node.children[i]
end
obj
end
def of_coq_object(node)
of_coq_object node
end
end
module ToXml
extend self
[:quit, :getoptions, :about, :status, :goal, :evars, :hints].each do |meth|
define_method meth do
call meth
end
end
def interp(str, opts = {})
call 'interp', opts do |xml|
xml.text str
end
end
def rewind(steps)
call 'rewind', steps: steps
end
def mkcases(str)
call 'mkcases' do |xml|
xml.text str
end
end
# name_pattern: RegExp
# type_pattern: String
# subtype_pattern: String
# in_module: Array<String>
def search(opts)
call 'search' do |xml|
[:name_pattern, :type_pattern, :subtype_pattern].each do |key|
if opts.has_key? key
search_constraint xml, key do
xml.string do
xml.text opts[key]
end
end
end
end
if opts.has_key? :in_module
search_constraint xml, :in_module do
xml.list do
opts[:in_module].each do |s|
xml.string do
xml.text s
end
end
end
end
end
end
end
private
def call(meth, opts = {}, &blk)
Nokogiri::XML::Builder.new do |xml|
xml.call({val: meth}.merge(opts)) do
blk.call xml if blk
end
end.to_xml
end
def search_constraint(xml, key, &blk)
xml.pair do
xml.search_constraint val: key, &blk
xml.bool val: true
end
end
end
class CoqtopSlave
BUFSIZ = 1<<22
def initialize(io)
@io = io
end
[
:about,
:getoptions,
:status,
:quit,
:goal,
:evars,
:hints,
:interp,
:rewind,
:mkcases,
:search,
].each do |meth|
define_method meth do |*args|
@io.puts ToXml.public_send meth, *args
doc = Nokogiri::XML.parse @io.readpartial(BUFSIZ)
FromXml.convert doc.root
end
end
end
require 'awesome_print'
begin
IO.popen(['coqtop', '-ideslave'], 'r+') do |io|
slave = CoqtopSlave.new io
puts 'About'
ap slave.about
# puts 'Options'
# ap slave.getoptions
puts 'Initial status'
ap slave.status
puts 'mkcases nat'
p slave.mkcases('nat')
puts 'mkcases list'
p slave.mkcases('list')
puts 'Search by name: .*iter'
ap slave.search(name_pattern: /.*iter/.source)
puts 'Search by type: nat -> nat'
ap slave.search(type_pattern: 'nat -> nat')
puts 'Search by module: Coq.Init.Peano'
ap slave.search(in_module: %w[Coq Init Peano])
puts 'Theorem'
slave.interp("Theorem t : forall n m : nat, n + m = n + m.")
ap slave.status
ap slave.goal
ap slave.evars
puts 'Do intro'
slave.interp("intro.")
ap slave.status
ap slave.goal
ap slave.evars
puts 'Hints'
ap slave.hints
puts 'Do intro'
slave.interp("intro.")
ap slave.status
ap slave.goal
ap slave.evars
puts 'Rewind 1'
p slave.rewind(1)
ap slave.status
ap slave.goal
ap slave.evars
puts 'Do reflexivity'
slave.interp("reflexivity.")
ap slave.status
ap slave.goal
ap slave.evars
puts 'Do Qed'
slave.interp("Qed.")
ap slave.status
slave.quit
end
rescue FromXml::MappingError => e
$stderr.puts "MappingError: #{e.message}"
$stderr.puts e.node.to_xml(indent: 2)
e.backtrace.each do |bt|
$stderr.puts " #{bt}"
end
end
Raw
output.txt
About
{
:version => "8.4",
:protocol => "20120710",
:release => "May 2013",
:compile => "May 02 2013 22:02:15"
}
Initial status
{
:path => [
[0] "Top"
],
:proofname => nil,
:allproofs => [],
:statenum => 1,
:proofnum => -1
}
mkcases nat
[["O"], ["S", "x"]]
mkcases list
[["nil"], ["cons", "x", "x0"]]
Search by name: .*iter
[
[0] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter_invariant",
:object => "forall (n : nat) (A : Type) (f : A -> A) (P : A -> Prop),\n(forall x : A, P x -> P (f x)) -> forall x : A, P x -> P (nat_iter n f x)"
},
[1] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter_plus",
:object => "forall (n m : nat) (A : Type) (f : A -> A) (x : A),\nnat_iter (n + m) f x = nat_iter n f (nat_iter m f x)"
},
[2] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter_succ_r",
:object => "forall (n : nat) (A : Type) (f : A -> A) (x : A),\nnat_iter (S n) f x = nat_iter n f (f x)"
},
[3] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter",
:object => "nat -> forall A : Type, (A -> A) -> A -> A"
}
]
Search by type: nat -> nat
[
[0] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "pred",
:object => "nat -> nat"
},
[1] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Datatypes"
],
:qualid => "S",
:object => "nat -> nat"
}
]
Search by module: Coq.Init.Peano
[
[ 0] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter_invariant",
:object => "forall (n : nat) (A : Type) (f : A -> A) (P : A -> Prop),\n(forall x : A, P x -> P (f x)) -> forall x : A, P x -> P (nat_iter n f x)"
},
[ 1] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter_plus",
:object => "forall (n m : nat) (A : Type) (f : A -> A) (x : A),\nnat_iter (n + m) f x = nat_iter n f (nat_iter m f x)"
},
[ 2] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter_succ_r",
:object => "forall (n : nat) (A : Type) (f : A -> A) (x : A),\nnat_iter (S n) f x = nat_iter n f (f x)"
},
[ 3] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_iter",
:object => "nat -> forall A : Type, (A -> A) -> A -> A"
},
[ 4] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "min_r",
:object => "forall n m : nat, m <= n -> min n m = m"
},
[ 5] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "min_l",
:object => "forall n m : nat, n <= m -> min n m = n"
},
[ 6] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "max_r",
:object => "forall n m : nat, n <= m -> max n m = m"
},
[ 7] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "max_l",
:object => "forall n m : nat, m <= n -> max n m = n"
},
[ 8] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "min",
:object => "nat -> nat -> nat"
},
[ 9] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "max",
:object => "nat -> nat -> nat"
},
[10] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_double_ind",
:object => "forall R : nat -> nat -> Prop,\n(forall n : nat, R 0 n) ->\n(forall n : nat, R (S n) 0) ->\n(forall n m : nat, R n m -> R (S n) (S m)) -> forall n m : nat, R n m"
},
[11] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "nat_case",
:object => "forall (n : nat) (P : nat -> Prop), P 0 -> (forall m : nat, P (S m)) -> P n"
},
[12] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "le_S_n",
:object => "forall n m : nat, S n <= S m -> n <= m"
},
[13] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "le_pred",
:object => "forall n m : nat, n <= m -> pred n <= pred m"
},
[14] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "gt",
:object => "nat -> nat -> Prop"
},
[15] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "ge",
:object => "nat -> nat -> Prop"
},
[16] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "lt",
:object => "nat -> nat -> Prop"
},
[17] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "le_ind",
:object => "forall (n : nat) (P : nat -> Prop),\nP n ->\n(forall m : nat, n <= m -> P m -> P (S m)) ->\nforall n0 : nat, n <= n0 -> P n0"
},
[18] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "le_S",
:object => "forall n m : nat, n <= m -> n <= S m"
},
[19] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "le_n",
:object => "forall n : nat, n <= n"
},
[20] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "minus",
:object => "nat -> nat -> nat"
},
[21] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "mult_n_Sm",
:object => "forall n m : nat, n * m + n = n * S m"
},
[22] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "mult_n_O",
:object => "forall n : nat, 0 = n * 0"
},
[23] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "mult",
:object => "nat -> nat -> nat"
},
[24] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "plus_Sn_m",
:object => "forall n m : nat, S n + m = S (n + m)"
},
[25] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "plus_n_Sm",
:object => "forall n m : nat, S (n + m) = n + S m"
},
[26] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "plus_O_n",
:object => "forall n : nat, 0 + n = n"
},
[27] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "plus_n_O",
:object => "forall n : nat, n = n + 0"
},
[28] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "plus",
:object => "nat -> nat -> nat"
},
[29] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "n_Sn",
:object => "forall n : nat, n <> S n"
},
[30] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "O_S",
:object => "forall n : nat, 0 <> S n"
},
[31] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "IsSucc",
:object => "nat -> Prop"
},
[32] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "not_eq_S",
:object => "forall n m : nat, n <> m -> S n <> S m"
},
[33] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "eq_add_S",
:object => "forall n m : nat, S n = S m -> n = m"
},
[34] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "pred_Sn",
:object => "forall n : nat, n = pred (S n)"
},
[35] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "pred",
:object => "nat -> nat"
},
[36] {
:prefix => [
[0] "Coq",
[1] "Init",
[2] "Peano"
],
:qualid => "eq_S",
:object => "forall x y : nat, x = y -> S x = S y"
}
]
Theorem
{
:path => [
[0] "Top"
],
:proofname => "t",
:allproofs => [
[0] "t"
],
:statenum => 2,
:proofnum => 1
}
{
:fg => [
[0] {
:id => "2",
:hyp => [],
:ccl => "forall n m : nat, n + m = n + m"
}
],
:bg => []
}
[
[0] "?2 : [ |- forall n m : nat, n + m = n + m] "
]
Do intro
{
:path => [
[0] "Top"
],
:proofname => "t",
:allproofs => [
[0] "t"
],
:statenum => 3,
:proofnum => 2
}
{
:fg => [
[0] {
:id => "3",
:hyp => [
[0] "n : nat"
],
:ccl => "forall m : nat, n + m = n + m"
}
],
:bg => []
}
[
[0] "?3 : [n : nat |- forall m : nat, n + m = n + m] "
]
Hints
[
[0] [
[0] [
[ 0] [
[0] "clear n",
[1] "clear n.\n"
],
[ 1] [
[0] "apply n",
[1] "apply n.\n"
],
[ 2] [
[0] "exact n",
[1] "exact n.\n"
],
[ 3] [
[0] "generalize n",
[1] "generalize n.\n"
],
[ 4] [
[0] "absurd <n>",
[1] "absurd nat.\n"
],
[ 5] [
[0] "discriminate n",
[1] "discriminate n.\n"
],
[ 6] [
[0] "injection n",
[1] "injection n.\n"
],
[ 7] [
[0] "rewrite n",
[1] "rewrite n.\n"
],
[ 8] [
[0] "rewrite <- n",
[1] "rewrite <- n.\n"
],
[ 9] [
[0] "elim n",
[1] "elim n.\n"
],
[10] [
[0] "inversion n",
[1] "inversion n.\n"
],
[11] [
[0] "inversion clear n",
[1] "inversion_clear n.\n"
]
]
],
[1] [
[ 0] [
[0] "intro",
[1] "intro.\n"
],
[ 1] [
[0] "intros",
[1] "intros.\n"
],
[ 2] [
[0] "intuition",
[1] "intuition.\n"
],
[ 3] [
[0] "reflexivity",
[1] "reflexivity.\n"
],
[ 4] [
[0] "discriminate",
[1] "discriminate.\n"
],
[ 5] [
[0] "symmetry",
[1] "symmetry.\n"
],
[ 6] [
[0] "assumption",
[1] "assumption.\n"
],
[ 7] [
[0] "omega",
[1] "omega.\n"
],
[ 8] [
[0] "ring",
[1] "ring.\n"
],
[ 9] [
[0] "auto",
[1] "auto.\n"
],
[10] [
[0] "eauto",
[1] "eauto.\n"
],
[11] [
[0] "tauto",
[1] "tauto.\n"
],
[12] [
[0] "trivial",
[1] "trivial.\n"
],
[13] [
[0] "decide equality",
[1] "decide equality.\n"
],
[14] [
[0] "simpl",
[1] "simpl.\n"
],
[15] [
[0] "subst",
[1] "subst.\n"
],
[16] [
[0] "red",
[1] "red.\n"
],
[17] [
[0] "split",
[1] "split.\n"
],
[18] [
[0] "left",
[1] "left.\n"
],
[19] [
[0] "right",
[1] "right.\n"
]
]
]
Do intro
{
:path => [
[0] "Top"
],
:proofname => "t",
:allproofs => [
[0] "t"
],
:statenum => 4,
:proofnum => 3
}
{
:fg => [
[0] {
:id => "4",
:hyp => [
[0] "n : nat",
[1] "m : nat"
],
:ccl => "n + m = n + m"
}
],
:bg => []
}
[
[0] "?4 : [n : nat m : nat |- n + m = n + m] "
]
Rewind 1
0
{
:path => [
[0] "Top"
],
:proofname => "t",
:allproofs => [
[0] "t"
],
:statenum => 3,
:proofnum => 2
}
{
:fg => [
[0] {
:id => "3",
:hyp => [
[0] "n : nat"
],
:ccl => "forall m : nat, n + m = n + m"
}
],
:bg => []
}
[
[0] "?3 : [n : nat |- forall m : nat, n + m = n + m] "
]
Do reflexivity
{
:path => [
[0] "Top"
],
:proofname => "t",
:allproofs => [
[0] "t"
],
:statenum => 4,
:proofnum => 3
}
{
:fg => [],
:bg => []
}
[]
Do Qed
{
:path => [
[0] "Top"
],
:proofname => nil,
:allproofs => [],
:statenum => 5,
:proofnum => -1
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment