Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9202280204.AA27480@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: Strange behavior of quotation parser & a question
Date: Thu, 27 Feb 92 18:04:25 PST
From: chou@edu.ucla.cs

Sigh!  For some reason I always got into trouble with HOL quotation
parser.  I have a theory `tla`, which contains (among other things)
these definitions:

new_definition(`map_binary_DEF`, "
  map_binary (op : *2 -> *1 -> *0) (A2 : * -> *2) (A1 : * -> *1)
  = \ x : * . op (A2 x) (A1 x)
") ;;
new_infix_definition(    `and_DEF`, "
  $and   : (* -> bool) -> (* -> bool) -> (* -> bool) = map_binary $/\
") ;;
new_infix_definition(     `or_DEF`, "
  $or    : (* -> bool) -> (* -> bool) -> (* -> bool) = map_binary $\/
") ;;

The following happened:

#load_theory `tla` ;;
Theory tla loaded
() : void

#"((A:*->bool) and B or C)" ;;
"A and (B or C)" : term

#"((A:*->bool) and B or X and Y)" ;;
"A and (B or (X and Y))" : term

#"((A:*->bool) and B or X and Y" ;;
bad paren balance
skipping: Y " ;; parse failed

#"((A:*->bool) and B or X and Y)" ;;
Badly typed application of:  "A"
   which has type:           ":* -> bool"
to the argument term:        "$and"
   which has type:
    ":(?1 -> bool) -> ((?1 -> bool) -> (?1 -> bool))"

evaluation failed     mk_comb in quotation

#"((A:*->bool) and B or C)" ;;
Badly typed application of:  "A"
   which has type:           ":* -> bool"
to the argument term:        "$and"
   which has type:
    ":(?1 -> bool) -> ((?1 -> bool) -> (?1 -> bool))"

evaluation failed     mk_comb in quotation


It seems that the quotation parser has memory of previous failures.
The above was performed by an AKCL HOL2.0.

A question: Is there a way to specify precedences for defined infixes?

- Ching Tsun