HimML is an implementation of a variant of the functional imperative higher-order language Standard ML, with native set and map operations. A short description was published at the ML workshop in 1994.
Download HimML α 20
Precompiled packages:
- HimML α 20 For MacOSX, x86_64 architecture (Intel, AMD64)
- HimML α 20 For Linux/Ubuntu (Debian), x86_64 architecture (Intel, AMD64)
Or download the source distribution. Then type:
cd Alpha20
- (optionally review file
OPTIONS
beforehand, notably if you wish to change the final installation directory) ./makemake
make
make install
You should now have a working HimML installation, with new commands installed in /usr/local/bin
(make sure to include it in your PATH
variable):
- The HimML toplevel:
himml
- The HimML bytecode compiler:
himmlc
- The HimML bytecode interpreter:
himmlrun
- The HimML lexical analyzer generator:
hlex
- The HimML parser generator:
hyacc
- The HimML dependency generator (meant to be use to populate makefiles):
himmldep
- The HimML linker and library archiver:
himmllnk
- The HimML package creator (used by
himmllnk
):himmlpack
- The HimML bytecode to native code compiler (requires
gcc
):himmlx
- The C include file used by
himmlx
:himmlx.h
(should be in your include file, typically/usr/local/include
) - The support library for
himmlx
:libhimml.a
(should be in your library path, typically/usr/local/lib
) - The HimML Emacs mode:
himml-mode.el
, and the site file:himml-site.el
Documentation
- The HimML language: online or as a pdf file.
- The
hlex
lexical analyzer generator: pdf. - The
hyacc
parser generator: online, or pdf.
A quick peek at HimML
Here are a few things you can write in HimML.
The following declares a type of first-order terms, where application is written using an operator $
. This is just as in Standard ML. A term is either a variable, for example V "x"
(standing for x), or an application, say "f" $ [V "x"]
(standing for f(x)).
The following declares a type of first-order terms, where application is written using an operator $
. This is just as in Standard ML. A term is either a variable, for example V "x"
(standing for x), or an application, say "f" $ [V "x"]
(standing for f(x)).
infix 0 $
datatype term = V of string
| $ of string * term listi
Now here is something particular to HimML. A substitution theta
is a map from variable names (of type string
) to terms. A HimML map is just a table: you may think of it as a hash table; if you are more mathematically minded, it is a function with finite domain.
It is easy to define a substitution function tsubst
, which applies a substitution theta
to a term t
. I will give the definition below. Its type is:
tsubst : (string -m> term) -> term -> term
Note that the type of maps from string
to term
is written with the map arrow operator -m>
. Let us apply it to an example. We define two constants a
and b
, helper functions to build applications of function symbols f
and g
, then two terms t1
and t2
. theta
is our first substitution!
val a = "a" $ []; (* the constant a *)
val b = "b" $ []; (* the constant b *)
fun f (s, t) = "f" $ [s, t]; (* applying the binary function symbol f *)
fun g (t) = "g" $ [t]; (* applying the unary function symbol g *)
val t1 = f (a, g (a)); (* a first term *)
val t2 = f(a,f(b,g(f(a,b)))); (* a second term *)
val theta = {"x" => t1, "y" => t2}; (* a substitution *)
Now can you guess what the following term will evaluate to?
tsubst theta (f (V "x", V "y"));
Try it under the HimML toplevel, and compare that to the expected term f (t1
, t2
) = f(f(a,g(a)), f(a,f(b,g(f(a,b))))).
Oh, and here is the definition of tsubst
, in case you would like to see how it is done.
fun tsubst (theta : string -m> term) =
let fun tsubst_theta (V x) =
if x inset theta (* if x is in the domain of theta *)
then ?theta x (* read off the value associated with x in theta, *)
else V x
| tsubst_theta (f $ l) =
f $ [tsubst_theta t | t in list l] (* list comprehension *)
in
tsubst_theta
end;
Applications
The H1 tool suite was almost entirely written in HimML.