Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Wed, 29 Apr 1992 13:15:02 -0700
From: hall@edu.uidaho.cs.cheetah
Message-Id: <199204292015.AA22888@cheetah.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Problems with inject_input and ML_eval in 2.0b?

Hi all,

I'm having some problems getting inject_input and ML_eval to work.
Maybe someone out there can help me?

Here's my problem:  I want to evaluate a string containing an ML 
function.  The functions is valid, but I get bizzare errors when
I send it to ML_eval.  Here's my example...
Notice, the string is terminated by the requisite semi-colons and
a newline (ascii 10).
-----------------------------------------------

#let str = 
`let (((REG' i) out18_val) REG19_val) = let (out t) = (if (t = 0) then\
 out18_val else (i (t - 1))) in out;;
`;;
str = 
`let (((REG' i) out18_val) REG19_val) = let (out t) = (if (t = 0) then\
 out18_val else (i (t - 1))) in out;;
`
: string
Run time: 0.0s

#ML_eval str;;
() : void
Run time: 0.0s

#2+2;;                           % I get the prompt again, but no eval %
) cannot be a var                % of the string, so I enter something %
skipping: ) ) ) in out ;; parse failed     

2 : int
Run time: 0.0s

-----------------------------------------------
And this also happens with inject_input...
-----------------------------------------------

#let int_str = (map ascii_code (explode str));;
int_str = 
[108; 101; 116; 32; 40; 40; 40; 82; 69; 71; 39; 32; 105; 41; 32; 111;
 117; 116; 49; 56; 95; 118; 97; 108; 41; 32; 82; 69; 71; 49; 57; 95;
 118; 97; 108; 41; 32; 61; 32; 108; 101; 116; 32; 40; 111; 117; 116;
 32; 116; 41; 32; 61; 32; 40; 105; 102; 32; 40; 116; 32; 61; 32; 48;
 41; 32; 116; 104; 101; 110; 32; 111; 117; 116; 49; 56; 95; 118; 97;
 108; 32; 101; 108; 115; 101; 32; 40; 105; 32; 40; 116; 32; 45; 32; 49;
 41; 41; 41; 32; 105; 110; 32; 111; 117; 116; 59; 59; 10]
: int list
Run time: 0.1s

#inject_input int_str;;
() : void
Run time: 0.0s

#2+2;;                           % again, no prompt %
) cannot be a var
skipping: ) ) ) in out ;; parse failed     

2 : int
Run time: 0.0s

-----------------------------------------------
It seems like beginning of `2+2` is getting appended on to the ML_eval
stuff.

Before you decide that the REG' function doesn't work, here's an odd
bit of information...
-----------------------------------------------

#let port = openw `junk.ml`;;
port = 
`#<Stream OSI-BUFFERED-STREAM "/usr/home/users/student/hall/hol/\
work/junk.ml" 10EFD9E6>`
: string
Run time: 0.0s

#write (port,str);;
() : void
Run time: 0.0s

#close port;;
() : void
Run time: 0.0s

#loadt `junk.ml`;;

REG' = - : ((int -> *) -> * -> ** -> int -> *)
Run time: 0.1s


File junk.ml loaded
() : void
Run time: 0.2s

-----------------------------------------------
Just for example, here's a function that works like I'd expect:
-----------------------------------------------

#let str =
`let ((AND' i1) i2) = let (out t) = ((i1 t) & (i2 t)) in out;;
`;;
str = 
`let ((AND' i1) i2) = let (out t) = ((i1 t) & (i2 t)) in out;;
`
: string
Run time: 0.0s

ML_eval str;;
() : void
Run time: 0.1s

AND' = - : ((* -> bool) -> (* -> bool) -> * -> bool)
Run time: 0.0s

% if you care... %
#map ascii_code (explode str);;
[108; 101; 116; 32; 40; 40; 65; 78; 68; 39; 32; 105; 49; 41; 32; 105;
 50; 41; 32; 61; 32; 108; 101; 116; 32; 40; 111; 117; 116; 32; 116; 41;
 32; 61; 32; 40; 40; 105; 49; 32; 116; 41; 32; 38; 32; 40; 105; 50; 32;
 116; 41; 41; 32; 105; 110; 32; 111; 117; 116; 59; 59; 10]
: int list
Run time: 0.0s

-----------------------------------------
I'm confused.  Why did the first string not work?  Why did the second?
Since writing the string and then loading it via a file works, I'm
led to believe a problem exists in inject_input / ML_eval.

What do the pros think?

I'm using HOL 2.0b [Lucid] on a DEC 5000, and I've checked my results
on a `clean' HOL session - no other variables set, no theories, et al,
just what I get after starting up HOL.

Thanks for any advice,

Kelly Hall     hall@cheetah.cs.uidaho.edu