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.
--
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
