Parsing `lfind_eval` output
Opened this issue · 1 comments
yalhessi commented
There's a problem with parsing the output of lfind_eval when I run with CoqSynth. This doesn't exist when using myth because myth does extraction instead of parsing the output directly.
This can be replicated when run with even_list where it tries to evaluate Even so the value returned is actually a prop.
yalhessi commented
After looking more at the output here, here's one case that's handled correctly by the code we currently have:
= Cons 4 (Cons 4 (Cons 4 (Cons 4 (Cons 4 Nil))))
: lst
= Cons 1 (Cons 1 (Cons 1 Nil))
: lst
= Cons 2 (Cons 2 (Cons 2 (Cons 2 (Cons 2 (Cons 2 Nil)))))
: lst
= Cons 2 Nil
: lst
= Cons 3 (Cons 3 (Cons 3 (Cons 3 Nil)))
: lst
= Nil
: lst
= Nil
: lst
= Nil
: lst
= Cons 2 (Cons 2 Nil)
: lst
= Cons 6 Nil
: lst
= Cons 0 Nil
: lst
= Cons 0 (Cons 0 Nil)
: lst
= Cons 3 (Cons 3 Nil)
: lst
= Nil
: lst
= Cons 1 Nil
: lst
= Cons 4 (Cons 4 (Cons 4 Nil))
: lst
= Cons 4 (Cons 4 Nil)
: lst
= Nil
: lst
Here's a different case that's not handled:
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
= fun x : nat =>
exists x0 : nat,
x =
(fix Ffix (x1 : nat) : nat :=
match x1 with
| 0 => 0
| S x2 => S (S (Ffix x2))
end) x0
: nat -> Prop
From the second example, it's clear we need regex here to look forward when we're matching so to fix this we need to figure out how to include a regex library.