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
