John Harrison pointed out that my Mizar-like function `consider' and `cases' I
just posted won't work if a string contains /\ followed immediately by a
newline. We see the problem from
# "move (B,A,C) (B,A,X) /\ move (B,A,X) (B',A,X) /\
move (B',A,X) (B',A,Y) /\ move (B',A,Y) (B',A',Y)";;
val it : string =
"move (B,A,C) (B,A,X) /\\ move (B,A,X) (B',A,X) /move (B',A,X) (B',A,Y)
/\\ move (B',A,Y) (B',A',Y)"
Moving the /\ to the next line solves the problem, but that's not a nice
solution, and I thought I'd use backquotes instead of doublequotes. So I need
a function TermToString that just literally translates a backquoted expression
to the correct doublequoted expression (of course fixing backslashes and
newlines), without introducing any extra type inference, so
TermToString `M such that M = transp(vector[v:real^2;w:real^2]):real^2^2`
should evaluate to
"M such that M = transp(vector[v:real^2;w:real^2]):real^2^2"
This is a small part of what Freek Wiedijk must have done in moving from miz2
to miz3. I've looked pretty carefully in both the HOL Light dox and the HOL4
dox and can't find anything. I'm wondering if there's not something about
Ocaml that I'm missing.
Page 159 of the HOL4 Description manual says, "The parser turns strings into
terms." Doesn't that mean that backquoted expressions get turned into strings?
Now HOL4 seems a bit different from HOL Light, as
[P. 173] Thus the function Parse.Term function takes a (term) quotation and
returns a term,
and is thus of type
term quotation -> term
Now the HOL Light parse_term has type string -> term. I do think that HOL4 and
HOL Light both mean the same thing by quotation, an expression delimited by
single backquotes (called back-ticks by HOL4). The HOL Light tutorial says on
p 10 that "backquotes are used for quotations."
As par as I've gotten is to learn a bit about term_of_preterm and
preterm_of_term, which I believe are inverse functions. I can make little
sense of the large output from
preterm_of_term `M = transp(vector[v:real^2;w:real^2]):real^2^2`;;
but this evaluates to true
let foo = `M = transp(vector[v:real^2;w:real^2]):real^2^2` in
term_of_preterm (preterm_of_term foo) = foo;;
and that indicates to me that preterm_of_term is not introducing too many extra
type annotations. This however evaluates to false:
term_of_preterm (preterm_of_term `M =
transp(vector[v:real^2;w:real^2]):real^2^2`) =
`M = transp(vector[v:real^2;w:real^2]):real^2^2`;;
and I'm suspecting the reason is that some type annotation is taking place. In
fact:
# preterm_of_term `M`;;
Warning: inventing type variables
val it : preterm = Varp ("M", Utv "?84705")
# preterm_of_term `M`;;
Warning: inventing type variables
val it : preterm = Varp ("M", Utv "?84706")
Looks to me that 2 separate arbitrary types were assigned to M. So I guess I
don't know if preterm_of_term can be used to build my TermToString. Maybe
TermToListOfCharacters would be just as good, as long as there was an inverse
function.
BTW the problem I'm trying to solve is pretty simple. I want cases to have
multiple arguments which are terms, say `t1`, `t2` and `t3`, but I only want to
make as many give type annotations as I would need for
`t1 \/ t2 \/ t3`. I don't want to repeate type annotations in t1, t2 and t3.
--
Best,
Bill
------------------------------------------------------------------------------
Own the Future-Intel(R) Level Up Game Demo Contest 2013
Rise to greatness in Intel's independent game demo contest. Compete
for recognition, cash, and the chance to get your game on Steam.
$5K grand prize plus 10 genre and skill prizes. Submit your demo
by 6/6/13. http://altfarm.mediaplex.com/ad/ck/12124-176961-30367-2
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
