Hi Bill,
Short answer: string_of_term
Long answer:
let me try to make things clearer about what happens in HOL-Light
(pretty similar, conceptually, to what happens in HOL4) when you type in
something like `bla`:
1. the quotation `bla` is turned (by camlp5 indeed) into an expression
of type preterm
(this is done mainly by parse_preterm, preceded by "lex o explode")
2. the resulting preterm contains mostly no type information but the one
which is given explicitly in the term
3. the resulting preterm then goes through the function retypecheck
which checks that the preterm is well typed
4. then only it is turned into a value of type term by term_of_preterm
(note thus that a value of type term is assumed to be well-typed, which
is not the case for values of type preterm)
( Maybe the following example might make things clearer:
# parse_preterm (lex (explode "&1 + 1"));;
val it : preterm * lexcode list =
(Combp
(Combp (Varp ("+", Ptycon ("", [])),
Combp (Varp ("&", Ptycon ("", [])), Varp ("1", Ptycon ("", [])))),
Varp ("1", Ptycon ("", []))),
[])
# retypecheck [] (fst it);;
Exception: Failure "typechecking error (overload resolution)".
-> You see that the type error appears only after the call to
retypecheck, apart from that,
parse_preterm yields a very valid value of type preterm out of the
(badly-typed) expression "&1 + 1"
)
Consequence: each time you write `bla`, you automatically go through the
whole process of type inference.
Therefore, about your main problem, `t1` will automatically be given an
arbitrary type, as well as `t2` (and both type will be different, and
different from bool).
So there is no (simple) way to get a function disj_term that behaves the
way you want.
The alternative, that you seem to have considered already, is to use
strings (i.e., double-quote instead of single quote) but this yields the
problems you have already encountered (i.e., backslash preceding a new
line messes up the parsing).
The other alternative, which is the one you required in your previous
email, is to make use of the built-in term parser in order to avoid the
parsing problems of the first alternative, then go back to strings by
using a function that you called "TermToString", which exists in HOL
Light, except that it's called "string_of_term".
This might yield to other problems but I guess it will depend on the use
you make of it.
Cheers,
V.
Le 31.03.13 23:38, Bill Richter a écrit :
> Thanks, Ramana! You're the person I wanted to talk to. I already had a vague
> understand of what you explained (thanks for explaning), but I have a
> different question about HOL4:
>
> I'm convinced that the solution to my problem involves camlp (I use
> camlp5-6.05), as I can't find anything in the HOL Light or Ocaml dox. So I
> think this is a parsing issue, and I'd like to understand what HOL4 that's
> analogous to the HOL Light camlp5 parsing that allows us to put terms in
> backquotes (or back-ticks as the HOL4 dox say). So can you describe the what
> HOL4 does that's comparable to the HOL Light use of camlp? I bet it will be
> easier for me to understand. For starters, why does HOL4 use double
> backquotes instead of HOL Light's single backquotes?
>
> 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).
>
> That's encouraging for my project! I bet you're right. I bet preterm_of_term
> doesn't do type-inference and it's the later function term_of_preterm that
> does type-inference. Certainly the first place in preterm.ml where the
> string "infer" occurs is as an error message in term_of_preterm.
>
> Let me clarify what I want. Take two blocks of text t1 and t2. I want a
> functions like disj_term so that evaluating
>
> disj_term `t1` `t2`;;
>
> yields `t1 \/ t2`. That's not going to be possible if HOL Light does type
> inference on `t1` and `t2 before disj_term goes to work. And I'm sure from
> Freek's miz3 that HOL Light does not perform such type inference.
>
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
Own the Future-Intel® 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://p.sf.net/sfu/intel_levelupd2d
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
