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:

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

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.

— Jean Goubault-Larrecq.