The toplevel loop is not working at the moment... If you have ideas about the semantics and design of this, please contact us.

If you just type `"$ pml file.pml"`

, then PML will type-check and proof-check your file your file and it will run it and display the result. The available options are displayed using the `-h`

or `--help`

flag.

``examples/simple/first.pml``

openintvalsquare n = n*nvalbig = square 100

Example: if you have the (simple) program above in a file named `first.pml`

and type `"$ pml first.pml"`

in your favorite terminal, you should get:

Correct pml code

$ pml first.pml {valbig = int%10000valsquare =fun...}

Note that the value of the function `square`

is not displayed.

No compiler is available at the moment. An optimized llvm based compiler is planed for the near future.

You can "compile" a file using `$ pml -c file.pml`

. This will only type-check and proof-check the file without running it.

By opening the `int`

module, you can access the usual arithmetic operations on integers:

``examples/simple/second.pml``

openintvalx = 2+3*5valy = x*x-xvalz = y % 2

There is some *magic* that needs to be explained here. If you read the file `$PML_ROOT/lib/int.pml` from the distribution, you will see lines such as:

Correct pml code

valadd = int%add

This defines `add`

as an *internal* function (internal means not defined in PML) performing addition on the predefined data-type `int%`

. Then, the symbol `+`

will have access to **all** functions named `add`

and will disambiguate this using typing.

The same happens for constants. A constant of type `int`

should be written `int%123`

. When you write `123`

, PML does its best to guess what you actually mean...

Remark: `int`

is the type of integers of arbitrary size, currently using the `bignum`

library of OCaml. When compilation is available, it will probably correspond to GMP arbitrary precision integers. PML also knows about 32 and 64 bits integers (more sizes will be supported in the future, but we currently only support the sizes that are directly accessible in OCaml). Here is an example:

``examples/simple/third.pml``

openintopenint32openint64valx = 123456:int32valy = 1234567890:int64valz = 12345678901234567890:intvalx' = 2*x*x+1valy' = 2*y*y+1valz' = 2*z*z+1untyped(x'+y')

This example needs further explanation: The last line starting with the keyword `untyped`

means that the following expression should not be accepted (PML will display an error message if it is accepted). Here `x'`

is of type `int32`

and `y'`

is of type `int64`

and there is no `add`

function taking argument with such type. Language like C would automatically convert `x'`

to an `int64`

but this is considered harmful by the PML developers. Indeed, conversion from `int32`

to `int64`

is not a morphism in the mathematical sense, which means that the result of an expression using some conversion is not canonical.

It is very easy to define functions in PML. Let us start with an example:

Correct pml code

openintvaldouble n = n+nvalsquare =funn -> n*nvalnorm_square = \n p. square n+square pvalf n m p q = p*q+norm_square n m

We see here various syntaxes for function. The syntax `fun x y z ->`

is equivalent to `\x y z.`

and
when defining a value with the `val`

keyword, `val f x y z =`

is equivalent to `val f = fun x y z ->`

.

A very common error is to write the following:

Incorrect pml code (with error message)

Pml outputopenintvalpred x = x-1valtest = pred 3

Type error at /tmp/tmpS2V5y2.pml: line 3 column 11 to column 15: --- int% at line 3 column 16 to column 17 used as functions at line 2 column 13 to column 16

Here PML is detecting an error at the third line, saying that the
integer at the third line, in used as a function at the first line.
PML understood `x (-1)`

that is a function applied to `-1`

.
one should write `x- 1`

or better `x - 1`

.

One can also define recursive function as follows:

Correct pml code

openintopenboolvalrecfact n =ifn = 0then1elsen*fact (n-1)valrecfib n =ifn = 0 || n = 1then1elsefib (n-1)+fib (n-2)

We recognize here the classical factorial function and Fibonacci sequence.
Notice that the keyword `rec`

is mandatory to inform PML that we define a recursive function.
`val x = x + 1`

defines `x`

using the old value of another variable named `x`

. We say that
we are *shadowing* `x`

.

We can also define mutually recursive functions:

One can give local definitions. Here is the definition the arithmetico-geometric mean which is the limit we obtain by computing the arithmetic and geometric mean of two numbers and continuing until we reach the limit (here we take the arbitrary value of 50 to stop the loop:

``examples/simple/ag_average.pml``

openfloat64openintvalAG_average n m =letrecf i:int n m =ifi = 0thenmelsef (i-1) ((n+m)/2) (sqrt (n*m))inf 20 n m

Notice that in this example, we mix integer and floating point number.
For `n`

and `m`

, PML knows that they are float because of the use of
the function `sqrt`

which does not exist for integer. However, for the parameter
`i`

, we have to help PML by indicating its type at one place writing `i:int`

.

Lists are data structures which are very common in functional programming.
The syntax for finite list is `[x1;x2;x3;...]`

which includes the empty list as `[]`

. One can also add an element `x`

at the top of a list `l`

using the syntax `x::l`

. As an example, here is a function defining the list of integers from 1 to n:

Correct pml code

openintvalenum_int n =letrecfn acc p =ifp = 0thenaccelsefn (p::acc) (p-1)infn [] n

To read a given list, if you do not use the functions provided in the library `$PML_ROOT/lib/list.pml`, you need to use pattern matching. Let us start with an example,
the traditional `append`

function (sometimes named `concat`

) thats add all the elements of a first list at the top of the elements of a second list.

Correct pml code

valrecappend l1 l2 =matchl1with| [] -> l2 | x::l1' -> x::(append l1' l2)endmatch

One can see that pattern matching uses three keywords `match`

, `with`

and `endmatch`

. The last keyword is not mandatory to end pattern matching, but is necessary when using nested pattern matching. Between `match`

and `with`

is an expression that is computed and *matched* against each pattern occurring between the vertical bar and the arrow. A list matches the empty list pattern `[]`

if and only if it is the empty list. A list `l1`

matches the pattern `x::l1'`

if there exists two value `x`

and `l1'`

such that `l1`

is equal to `x::l1'`

. The variable `x`

and `l1'`

are bound in the right hand side of the pattern case. The result of pattern matching is the right hand side of the first pattern matching the given value.

One can also match more that the top element of a list. Here is an example:

Correct pml code

openboolvalrecis_sorted cmp l =matchlwith| [] | [_] ->true| x::(y::_asl) -> cmp x y && is_sorted cmp l

This function tests if a list is sorted by comparing adjacent
elements. One may notice the *or-pattern* in the first case,
matching both lists with 0 or 1 elements and the *catch-all* written
`_`

which avoid to waste unused identifier names. In the second cas,
one may notice the `as`

feature which allows to give a name both to
the tail of the list (here `l`

) and its second element (here `y`

).

Very often, one needs to manipulate (ordered) pairs, tripple, ... On common case for this are functions returning more than one values. This is not possible in traditional functional language, thus tuple are used for this.

The syntax for tuple is a comma separated sequence of expression. Parenthesis are not mandatory (in mathematics, they are) but it is a good practice to write them.

Here is a classical example: a function taking a list of pairs a returning two lists:

Correct pml code

valrecsplit l =matchlwith| [] -> [], [] | (x,y)::l' ->let(l1, l2) = split l'in((x::l1), (x::l2))endmatch

On may notice in this example the use of a pattern in a local definition. `let l1, l2 = split l' in x::l1, x::l2`

is a shortcut for a pattern matching with one cases.

One can write type definitions in PML and indicate the types of expressions in a program. But, what is a type ? It denotes a set of expressions and in fact in PML.

Here is a simple example:

Correct pml code

openintopenlisttypeseq = list(int)valsum : (seq -> int) =funl ->letrecfn acc l =matchlwith| [] -> acc | n::l' -> fn (n+acc) l'infn 0 lvaltest = sum [1;2;3;4;5;6;7;8;9;10]

Here we notice the definition of the type `seq`

as list of integers, using the type `int`

and `list`

from the libraries with the same names. We also remark that
the type list as one parameter (as expected). Then, in the definition of the `sum`

that computes the sum of all integers in the list, we remark that we first give its type `seq -> int`

meaning that it is a function taking a list of integer and returning an integer.

Here, we have seen *atomic* types like `int`

, `int32`

and function type written `t1 -> t2`

if `t1`

and `t2`

are types. There are other notion of types that we will introduce later.

We have also see type definition written:

Pseudo code

typet = ...

It is very useful when programming to consider data types that can have different cases for their values.
This is done by forming a *(disjoint) sum* or a *(polymorphic) variant*:

In fact lists are a particular case of variants with two cases: `[]`

which is an abbreviation for `Nil[]`

and `x::l`

which is an abbreviation from `Cons[x,l]`

.
The booleans `true`

and `false`

are also abbreviations for the variants `True[]`

and `False[]`

.

The first simple use of sums is for comparison. Indeed, it is often useful to perform a comparison test with three cases and for this, we use comparison function returning either `Less[]`

, `Equal[]`

or `Greater[]`

. The function `compare`

available for instance for `int`

does that. Here is an example of function computing the lexicographic combination of two comparisons:

Correct pml code

vallexicographic (cmp1, cmp2) (n, m) (n', m') =matchcmp1 n n'with| Equal[] -> cmp2 m m' | r -> rvallexicographic_int2 = lexicographic (int.compare, int.compare)valtest =openintinlexicographic_int2 (1,2) (1,3)

Here we see that the syntax of variants uses square bracket. Two variants with distinct names will be considered as distinct values by PML.

We can use sums for other data types. Here is for instance a function performing insertion in an ordered binary tree. The order is defined by the first argument of insertion and uses the constructor introduced in the previous example. We represent the tree with `left`

, `right`

as a left and right sons and `data`

as data by `Node[left,data,right]`

and the empty tree by `Nil[]`

(because PML has *polymorphic variants* we can reuse *constructors* among different data types).

Correct pml code

valrecinsert cmp data tree =matchtreewith[] -> Node[[],data,[]] | Node[left,data',right] ->matchcmp data data'withLess[] -> Node[insert cmp data left, data', right] | Greater[] -> Node[left, data', insert cmp data right] | Equal[] -> treeendmatchendmatch

Because PML uses polymorphic variant which means that many data structures can use the same constructor. This as the advantage of being able to write such function:

Correct pml code

valmerge_option o1 o2 =matcho1, o2withNone[], None[] -> None[] | None[], y -> y | x, _ -> x

This function can be used with o1 and o2 of arbitrary data-types except atomic type
like `int`

, `int32`

, `int64`

, `float64`

, ... More precisely, o1 and o2 can be arbitrary sum constructor, tuples, functions and structure that will be introduced below.

The following function definition is not accepted by PML:

Incorrect pml code (with error message)

Pml outputvalf x y =matchx, ywith| A[] , _ -> y | _ , A[] -> x | B[] , B[] -> B[]

Incomplete patterm matching at: /tmp/tmpS2V5y2.pml: line 2 column 4 to column 12

The reason is the following: pattern matching on tuples must match a Cartesian product. But if there is more than one case, in general, the values accepted by a list of patterns is a union of Cartesian products. Unfortunately, a union of products is not a product and there is no larger product included in a union of products.

In the above example, the following Cartesian products are covered by all cases: (? * [ A[] ]), ([ A[] ] * ?) and ([ A[] | B[] ] * [ A[] | B[] ]). Clearly, the two first cases would mean that the last pattern is useless. But PML's developers consider that disambiguation of deep pattern matching based on useless cases may be misleading.

To help PML, it is enough to give the type of `x`

and `y`

as follows:

Correct pml code

valf x y =match(x:[A[]|B[]]), (y:[A[]|B[]])with| A[] , _ -> y | _ , A[] -> x | B[] , B[] -> B[]

It may be clearer to give a name to the type:

Correct pml code

typeA_or_B = [A[]|B[]]valf x:A_or_B y:A_or_B =matchx, ywith| A[] , _ -> y | _ , A[] -> x | B[] , B[] -> B[]

Pseudo code

| ?x -> ...

`?x`

matches all the variants that are accepted by the right member of the case. There must be only finitely many possibilities. `?x`

can be used in deep pattern. In fact, `?x`

in a pattern in a syntactic sugar for
`(A1[_] | ... | An[_])`

is `A1`

, ..., `An`

is the largest list of pattern accepted by the right member of the case.

Here is an example of utilisation (the complete example can be found `$PML_ROOT/tests/eval.pml`).
The idea is to write two functions `eval_a_expr`

and `eval_p_expr`

working on separate variant types `a_expr`

and `p_expr`

and be able to do the union of the two functions in the `eval_all`

function.

Pseudo code

typea_expr (expr) = [ Add[expr] | ... ]typep_expr (expr) = [ Pair[expr] | ... ]valeval_a_expr rec_eval = function Add[x,y] -> rec_eval x+rec_eval y | ...valeval_p_expr rec_eval = function Pair[x,y] -> (rec_eval x, rec_eval y) | ...valreceval_all x =matchxwith| ?x -> eval_a_expr eval_all x | ?x -> eval_p_expr eval_all x

Remark: only the final function is recursive, the intermediate functions have an extra arguments `rec_eval`

which whose value will be given only in the final recursive function.

We have already seen tuple. In fact tuples are just a syntactic sugar for records. Moreover, records can be used as structures (also called modules). For instance, a pml file is nothing but a large records without the initial and final curly braces.

The syntax for records is a list of definition enclosed by curly braces. Basic definitions are given with the following syntaxes:

Pseudo code

{valx = ...valy = ...valz = ... }

or

Pseudo code

{ x = ...; y = ...; z = ...; }

Remark: `val`

and semicolon terminated definitions can be mixed, but one sometimes needs a semicolon at the end of a `val`

definition. This is why it is allowed to have a semicolon at the end of a definition introduced by the `val`

keyword.

Records can contain recursive or mutually recursive definition with the following syntax:

Pseudo code

{valrecf1 = ...andf2 = ... }

It can also contains type and recursive type definitions using the following syntax

Pseudo code

{typet0 = ...typerect1 = ...andt2 = ...

A section is dedicated to type later in this document.

When we build a record, eash field can be used to define the following fields (or even the same field when using
`rec`

. Here is an example:

Pseudo code

{valx = 1valy = x+1 }

The field identifier here is used both as a field ame used for projection and a binding name for the value in the rest of the record. Both name may be different is you wish:

Pseudo code

{valnumber_xasx = 1valnumber_y = x+1 }

To access the element of a record, one uses the *dot notation*. The following code
will evaluate to `A[]`

:

Pseudo code

letr = { a= A[]; b = B[] }inr.a

It is possible to define a record from an initial record even if we do not know the exact set of labels this record have. Moreover, a record has a default field, which can sometimes (we will see why later) be accessed without projection. The syntax for both feature is:

Pseudo code

{ rwith... }

or

Pseudo code

{ r | ... }

The above syntax can be used for any value of `r`

. If `r`

is not a record, then `r`

will
be the default field of the resulting record. For instance, if `r`

is a function, the whole record can
be applied to an argument. Here is an example:

Correct pml code

valr = {funx -> xwithvalid = A[] }valx = r B[]vala = r.id

This feature will be used a lot to add specifications to functions.

Sometimes one wants to remove/select some fields of the record `r`

, or one may want to prevent
some field to be present in r. Here is the syntax for that:

Pseudo code

{ r forbid l1,...,lnwith...} { r remove l1,...,lnwith...} { r select l1,...,lnwith...} { r authorize l1,...,lnwith...}

In the above, `forbid`

means that the field `l1,...,ln`

must be absent; `remove`

means that these
fields will be removed if present; `select`

means that we only keep the fields present in `r`

which are among the given fields and finally, `authorize`

means that no other fields than those given are present in `r`

.

These keywords can be combined together in any order as in the following example:

Pseudo code

{ r forbid a remove bwith...}

The keyword `fresh`

can be used in front of any definition to add it implicetely in the `forbid`

list.
`{ r with fresh a = ...; }`

is equivalent to `{r forbid a with a = ...; }`

.

One can pattern match records, with basically the same syntax (except
that `type`

can not be pattern matched, and the `rec`

keyword is
clearly useless in pattern). However, the default field can be used in
pattern to match the other fields. Here are the basic examples:

The following pattern match records which have exactly three fields
`l1`

, `l2`

and `l3`

:

Pseudo code

matchrwith{l1 = l1; l2 = l2; l3 = l3; } -> ...

or using the `val`

keyword:

Pseudo code

matchrwith{vall1 = l1vall2 = l2vall3 = l3; } -> ...

Because this looks a bit heavy, PML provides a shortcut when writing
`val l = l`

:

Pseudo code

matchrwith{l1; l2; l3; } -> ...

If you want to match a record whose fields are among `l1`

, `l2`

and `l3`

,
just add `...`

at the end of the record pattern:

Pseudo code

matchrwith{l1; l2; l3; ...} -> ...

To mtch the rest of the record, use the following syntax:

Pseudo code

matchrwith{otherwithl1; l2; l3} -> ...

or

Pseudo code

matchrwith{other | l1; l2; l3} -> ...

Here other will be bind to a record containing all the fields of
`r`

but `l1`

, `l2`

and `l3`

.

When matching the default field using a variant pattern, you may want to use
or not the `...`

at the end of the record pattern:

Pseudo code

matchrwith{A[] | l1; l2; l3} -> ...

matches records whose default field is `A[]`

and with exactly `l1`

, `l2`

and `l3`

as other field while

Pseudo code

matchrwith{A[_] | l1; l2; l3; ...} -> ...

matched records whose default field is `A[_]`

and wich have at least the fields `l1`

, `l2`

and `l3`

.

Pseudo code

{valx =: ...(* champs toujours inlinéschamps dont la valeur fait partie des contraintes de typesrestriction: ne peut parler que des champs précédentsdu même recordstatut à clarifier dans les « val rec »à l'intérieur des preuves *)

Le lieur n'est pas forcément le label:

Pseudo code

{valxastoto(* x est le nom du champ, mais on l'appelle totodans la suite du record *)

Exemple:

Pseudo code

{valxasy = ... ,valf = ... y ... }.x

Pseudo code

typetoto = {valsize : int,vala[0...size]: ...valb[1...size]: ...

même contrainte que pour « `=:`

»

Pseudo code

{ xwithval...includer(* recopie r(sauf le champ par défaut, et les champs qui sontécrasés après [note: en général, on ne peut pas écrire:{ val l = ... , val l = ... }])il est nécessaire de connaître tous les champs de ren particulier le champ par défaut de r ne doit pasêtre un record indéterminé (cette restriction nes'applique pas à x, qu'on est en train d'étendre) *)

Note:

- le champ par défaut: analogue dua
`_`

dans le pattern matching - le
`?x`

du pattern matching: dual du include

PML provides two distincts mechanisms to deal with errors:

*exceptions*(à la Caml, Python, Java...),*errors*.

The difference between the two is that while errors will always exit the program, exceptions can be caught, inspected and acted upon, either to exit the program or to try to correct something.

Explicitly provoking an error / exception is easy:

Pseudo code

valmy_function args = ...raiseexc(* exception *)...errorer(* error *)

Both errors and exceptions are special cases of values, and they explicitly appear in function types. The type of a function is specified by four types:

- the type of the argument,
- the type of the return value (neither exceptional nor erroneous),
- the type of the possible exceptions,
- the type of the possible errors.

A typical type of a function thus looks like

Pseudo code

valrecf : (list int -> int | [Invalid_Argument[]] | [Loop[]]) x = ...

Exceptions and/or errors can be empty:

Pseudo code

valrecf : (list int -> int | [Invalid_Argument[]] | []) x = ...

and PML defines A => B as a synonym for A -> B | [] | [], that is, a function which raises no exception and no error.

Similarly, A -> B is a synonym for A -> B | ? | ?, that is, a function that can raise any error and any exception.

In the default configuration, neither errors nor exceptions are authorized at the "file" level:

Incorrect pml code (with error message)

Pml outputvalpb =raise(undef[])

Type error at /tmp/tmpS2V5y2.pml: line 2 column 0 to column 0: --- variants "+undef" at line 1 column 16 to column 23 used as empty variants at line 2 column 0 to column 0

Trying to "compile" or open this file will fail.

Note that this is only true of exceptions / errors that are actually evaluated. The following is accepted because the function is already in evaluated form.

Correct pml code (with result)

Pml outputvalf x =raise(undef[])

However, the user can give a set of authorized exceptions and errors *in a given file* by putting #authorized_exception ... and / or #authorized_error ... at the very top of the file.
What follows #authorized_exception is a list of constructor names (without the brackets) separated by spaces.
The following file is thus a correct pml file:

Correct pml code (with result)

Pml output#authorised_exceptionundef Other_constructorvaltest1 = A[]valpb =raiseundef[]valtest2 = B[]

/tmp/tmpx4JERm.pml: line 4 column 12 to column 15 Exception: undef[]

"Compiling" this will succeed, but actually evaluating it, or opening it inside another file may fail if the exception `undef[]`

is not caught. Calling pml on this file will provoque a warning as the last line is never reached: "`Warning: dead code ...`

".

Not that since files are just like structures, neither `test1`

nor `test2`

are defined after reading this file.

The way this is typically used is when some value is defined using a function in another file:

#authorised_exceptionNot_foundopenlist ...valenvironment = ...valname = assoc eq_string "NAME" environment

Just like Caml, pml has a try ... with ... mechanism to allow inspection of exceptions. Exceptions are propagated "up" until they meet a try ... with ... or they reach top-level.

A typical example is

Correct pml code

openunary_natvalsub_trunc n m =(* compute the truncated substraction n-m *)trysub n mwithUndef[] -> 0

PML allows another construction: let try ... in ... with ... not readily available in Caml. It is used like

Pseudo code

valf x = ...lettrya = exp1inexp2withA[] -> ... | B[] -> ...

and the semantics is that only exceptions raised inside exp1 are handled by the with. Exceptions raised inside exp2 are propagated normally.

This construction has the same syntax as normal let ... in and thus allows simultaneaus local definitions to have the same handler:

Correct pml code (with result)

Pml outputopenunary_natvalf a b =lettrya' = pred(a)andb' = pred(b)ina'+b'withUndef[] -> 0valtest0 = f 0 0valtest1 = f 0 2valtest2 = f 2 0valtest3 = f 2 2

valtest0 = Z[]valtest1 = Z[]valtest2 = Z[]valtest3 = S[S[Z[]]] }

**Note:**
in fact, the primitive construction is let try .... The "usual" try ... with ... is just syntactic sugar for let try v = ... in v with ....

As opposed to Caml, any value can be raised. Thus, both raise {} and error (fun x->x) are valid PML. However, it is probably a very good idea to guard your exceptions and errors with specific constructors to avoid problems.

The only case when unguarded exception can be useful is when they are used as a local way of controlling flow of execution:

Correct pml code (with result)

Pml outputopenbinary_natvalrecmult =fun[] -> 1 | a::l ->if(a=0)thenraise0elsea*(mult l)valcompute f e =tryf ewithv -> vvaltest1 = compute mult [1;2;3;4;0;1;2;3;4]valtest2 = compute mult [1;2;3;4;5]

valmult =fun...valtest1 = End[]valtest2 = Zero[Zero[Zero[One[One[One[One[End[]]]]]]]] }

**TODO:**

- types
- polymorphisme
- subtilités sur except et without dans l'héritage (patterns et records)