Oh wait, I think I just found a quick (maybe dirty) hack: in the file
system.ml, replace the lines:
let quotexpander s =
if String.sub s 0 1 = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else "parse_term \""^(String.escaped s)^"\"";;
by:
let quotexpander s =
if String.sub s 0 1 = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else if String.sub s 0 1 = ";" then
"(fst o parse_preterm o lex o explode) \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else "parse_term \""^(String.escaped s)^"\"";;
Then each time you type something that starts with a semi-colon (e.g.,
`;blabla`), you obtain the intermediate preterm instead of the term.
If I'm right, this means that you don't have the backslash problem
anymore (since we're going through the John's parser), but not all the
types are infered since we didn't go through the type checking phasis
yet. And you could define a function disj_preterm easily (once you built
your preterm, it is easy to get the term by using term_of_preterm,
generally composed with retypecheck in order to check that the final
term is well typed).
I didn't go far in these thoughts though. So there might be other
loopholes that I'm not aware of.
V.
PS: I have the feeling that I have seen some quotations starting with
";" somewhere else, but I can't remember where, maybe there's a
connection, maybe not...?
Le 01.04.13 23:31, Vincent Aravantinos a écrit :
> Ok, got it. Indeed, I don't see any other options than the one already
> mentionned.
> The parser one is indeed the most complex of them but it's of course
> doable.
> I had the same problem when developping for HOL-Light a module similar
> to the Q module of HOL4 (see
> http://users.encs.concordia.ca/~vincent/Software.html).
> My own conclusion was that using strings was offering the best
> compromise time/benefit (compared to developping my own parser).
> The only drawback is that backslashes require a particular attention
> as you noticed already, but the implementation is much more
> straightforward than developping a new parser.
>
> Le 01.04.13 22:46, Bill Richter a écrit :
>> Thanks, Vincent! Let me be more precise. I want functions that act
>> on terms that are somewhat like the ocaml function ^ which
>> concatenates strings. I don't know how to define ^, but I know how
>> to define similar functions on lists in ocaml. There's a simple
>> example in the official documentation ocaml-4.00-refman.pdf on page
>> 12--13:
>>
>> let rec sort lst =
>> match lst with
>> [] -> []
>> | head :: tail -> insert head (sort tail)
>> and insert elt lst =
>> match lst with
>> [] -> [elt]
>> | head :: tail -> if elt <= head then elt :: lst else head ::
>> insert elt tail;;
>>
>> let l = ["is"; "a"; "tale"; "told"; "etc."];;
>>
>> sort l;;
>>
>> This is easy, but you have to know how lists work to do it, that
>> every list is either [] or of the sort head :: tail where tail is a
>> list. You'd have to know more things of that sort to understand how
>> to write ^. I think what I want is similar, but it requires
>> knowledge of the much harder camlp:
>>
>> Given two blocks of text t1 and t2 (I don't want to call them
>> strings), I want to define a function disj_term so that
>>
>> disj_term `t1` `t2`;;
>>
>> evaluates to the term `t1 \/ t2`. Now it's possible that this can't
>> be done, and it's also possible that Petros just did it. I think you
>> can't do this if you first apply string_of_term to the terms `t1` and
>> `t2`, because that will destroy explicit type annotations. That's
>> clear from the documentation:
>>
>> The call string_of_term tm produces a textual representation of the
>> term tm as a string, similar to what is printed automatically at
>> the toplevel, though without the surrounding quotes.
>>
>> That is, the toplevel textual representation has less information
>> than type_of will give you, so you lose explicit type annotations.
>> But I don't want to lose them. Let me give an example: I want
>>
>> disj_term `~collinear {B,(A:real^2),A'} /\ ~collinear {A',B,B'}`
>> `~collinear {A,B,B'} /\ ~collinear {B',A,A'}`;;
>>
>> to evaluate to
>>
>> `~collinear {B,(A:real^2),A'} /\ ~collinear {A',B,B'} \/ ~collinear
>> {A,B,B'} /\ ~collinear {B',A,A'}`
>>
>> It's important that I don't lose my type annotation A:real^2, because
>> that annotation forces B, A' and B' to also have type real^2. But
>> string_of_term would remove that type annotation A:real^2.
>>
>> So I figure that writing disj_term would require understanding how
>> the parser works, but if you did, it should be straightforward.
>>
>
>
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
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
