In HOL4, all code is passed through a "quotation filter" which does roughly
the following transformations:
`x y z ^(a b c) w` = [QUOTE "x y z ", ANTIQUOTE (a b c), QUOTE " w"]
``foo`` = Term`foo` = Term[...]
``:bar`` = Type`bar` = Type[...]
Term has type term frag list -> term.
Type has type hol_type frag list -> hol_type.
QUOTE has type string -> 'a frag.
ANTIQUOTE has type 'a -> 'a frag.
So much for the mechanincs of quotations in HOL4, which probably doesn't
help you much except for knowledge and peace of mind.
The real piece you need, however, is the fact that Term does
type-inference. I'm not sure if there is anything in HOL-Light already that
does type-inference (as opposed to type-checking).
For further information on how it's done, I would look at the HOL4 docfiles
for, for example Parse.Term, and possibly the sources under the src/parse
directory.
On Sat, Mar 30, 2013 at 3:53 AM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> 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
>
------------------------------------------------------------------------------
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
