Parser bugs summary

[u5943321]

"ALL X. ALL Y. ALL f0. ALL f1. isrefl(f0:X->Y,f1:X->Y) <=> EXISTS d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)"
fvf it;
val it =
HOLset{("f0", ar (Bound 3, Bound 2)), ("f0", ar (Bound 4, Bound 3)),
("f1", ar (Bound 3, Bound 2)), ("f1", ar (Bound 4, Bound 3))}:
(string * sort) set,

rapf "!X.!Y.!f0.!f1. isrefl(f0:X->Y,f1:X->Y) <=> ?d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)";
fvf it = {}
rapf "!X.!Y.!f0.!f1. isrefl(f0:X->Y,f1:X->Y) <=> ?d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)" = rpf "!X.!Y.!f0.!f1. isrefl(f0:X->Y,f1:X->Y) <=> ?d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)";
val it = true: bool
no extra change.

[u5943321]

rapg "~ (i1(X,X) o (t:1->X) = i2(X,X) o t)":

Exception- UNIFY "occurs check(pt):pv X : psv 1 ptu 1" raised

also need the "()" after "~"

---

after previous change, have:

rapf "i1(X,X) o (t:1->X) = i2(X,X) o t" = rpf " i1(X,X) o (t:1->X) = i2(X,X) o t"; and checked rpf does not need () as well, and works well with (), but do no extra edit.

[u5943321]

rapf "P(a) & P(b) ==> ALL s.Q(s) & Q(c)";
Exception- ERR "err in parsing bound variable" raised

not a problem, not accpeted by the parser because s is a constant, maybe raise a more helpful error message here.

[u5943321]

val f1 = rapf "~(EXISTS x1 : 1 -> X. EXISTS x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)";
Exception- UNIFY "occurs check(pt):pv X : psv 0 ptu 0" raised

rapf "(?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)" = rpf "(?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)";
val it = true: bool

rapf "?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1" = rpf "(?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)";
val it = true: bool

nothing extra.

[u5943321]

rapf "p2(A, B) o g:X->A * B = p2(A, B) o f" not an infix operator

---

rapf "p2(A, B) o g:X->(A * B) = p2(A, B) o f" = rpf "p2(A, B) o (g:X->A * B)= p2(A, B) o f";
val it = true: bool

() around A * B is critical. other wise it misread the formula and UNIFY complains. no extra change.

[u5943321]

rapf "((i:B->A) o m:A-> B) o h = (i o m) o g"
Exception- ERR "not an infix operator" raised

---

fixed 2021-6-30 2.47

[u5943321]

(rapf "h = eqinduce (f1:A-> B,f2,eqa(f1,f2) o g:X -> eqo(f1,f2))")

not an infix operator error

rapf "h = eqinduce (f1:A-> B,f2,eqa(f1,f2) o g:X -> eqo(f1,f2))" = rpf "h = eqinduce (f1:A-> B,f2,eqa(f1,f2) o g:X -> eqo(f1,f2))";
val it = true: bool

previous error caused by prec of : -> is too low.

[u5943321]

(rapg "~(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))")

Exception- UNIFY "occurs check(pt):i1 psv 4(1 pob,1 pob) ptu 4" raised

---

rapf "(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))" = rpf "(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))";
val it = true: bool

rapf "copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1))" = rpf "(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))";
val it = true: bool
rapf "~copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1))" = rpf "~copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1))";
val it = true: bool

after the edits, no extra change to fix this.

[u5943321]

rapf "~(EXISTS x0:1->A. a o x0 = x)";
Exception-
UNIFY "occurs check(pt):pv x0 : (1 pob,pob)-->(pv A : psv 0,pob) ptu 0"
raised

fixed in 2021-6.30 2 commit around 2.37.

[u5943321]

rapf "h o <id(AN),(f:AN->B)> = (f:A * N ->B) o <p1(A,N),s o p2(A,N)>"

if do not annotate the first f, it thinks the f is to C.

have rpf "h o pa(id(A * N),f) = f o pa(p1(A,N),s o p2(A,N))" = rapf "h o <id(A * N),(f:(A * N)->B)> = (f:(A * N) ->B) o <p1(A,N),s o p2(A,N)>";
val it = true: bool

rpf "h o pa(id(A * N),f) = f o pa(p1(A,N),s o p2(A,N))" = rapf "h o <id(A * N),f> = (f:(A * N) ->B) o <p1(A,N),s o p2(A,N)>";
val it = true: bool

after the previous edits, but do nothing extra.

[u5943321]

just record:

readf gives: val it = Pred ("<=>", [Var ("f", ob), Var ("g", ob)]): form
no need to edit if done with rapf.

[u5943321]

Think new parser is okay now, but want it to read formulas as !a b c (f:A->C)....

[u5943321]

"!A.!B.!X.!fg: X -> (A * B).!f: X -> A.!g: X -> B. p1(A,B) o fg = f & p2(A,B) o fg = g <=> fg = pa(f,g)"

need (A * B)

[u5943321]

want parser to parse !f:A * B ->C g:C->D. How to distinguish the space in A * B and the space between C and g?

[u5943321]

fvt (rastt"x0: X -> eqo(f:A->B,g)");
val it =
HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", ob),
("x0", X -> eqo(f, g))}: (string * sort) set

fvt (rastt"x0: X -> eqo(f:A->B,g:A->B)");
val it =
HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", A -> B),
("x0", X -> eqo(f, g))}: (string * sort) set

[u5943321]

fvt (rastt"x0: X -> eqo(f:A->B,g)");
val it =
HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", ob),
("x0", X -> eqo(f, g))}: (string * sort) set

fvt (rastt"x0: X -> eqo(f:A->B,g:A->B)");
val it =
HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", A -> B),
("x0", X -> eqo(f, g))}: (string * sort) set

---

fixed