swift-nav/plover

Plover is a language for matrix algebra on embedded systems.

Plover

Plover is an embedded Haskell DSL for compiling linear algebra into robust, efficient C code suitable for running on embedded systems.

Plover generates code free of dynamic memory allocation and provides compile time checking of matrix and vector shapes using a lightweight dependant type system.

Plover also aims to make use of sparse structure present in many real world linear algebra problems to generate more efficient code.

• Plover.Types contains the AST for the DSL.
• Plover.Expressions contains a number of example expressions.
• Plover.Reduce contains the main compiler.
• Plover.Macros contains DSL utilities.

Installation

First, install Stack or Haskell Platform. Key is having GHC 7.10+ available.

Check out the plover source:

$ git clone https://github.com/swift-nav/plover.git
$ cd plover

Then use one of the two available build methods.

Stack build

$ stack build

Run the test suite (requires gcc):

$ stack test

Installation of the plover binary into ~/.local/bin

$ stack build --copy-bins

or

# (equivalent to previous command)
$ stack install

(Alternative Installation Method) Cabal sandbox build

Using a cabal sandbox keeps any dependencies isolated so you don't have to worry about conflicts with other versions you may have on your system.

$ cabal sandbox init

Install the dependencies into the sandbox:

$ cabal install happy alex
$ cabal install --only-dependencies --enable-tests

Run the test suite (requires gcc):

$ cabal test --show-details=streaming

Usage

See http://swift-nav.github.io/plover/guide.html

plover's Issues

feature: easier __C__ blocks

currently specifying a block of inline C code is tedious and can only be done at the top level

• add a special syntax element, so we aren't using multiline strings for this
• figure out how to insert literal C blocks within functions

[docs] include builtin functions

plover/src/Language/Plover/Convert.hs

Line 144 in 4a0e671

builtinFuncs = [ ("not", builtinUFunc (\pos arg -> return $ T.Unary pos T.Not arg))

loop hoisting

need to hoist simple loop invariant things

Fixed point math

Is there any planned support for fixed point math for MCU's without a FPU? i.e Q16.16

hackage

get plover onto hackage

getting started

update
http://swift-nav.github.io/plover/guide.html

to point at main installation readme

several potential features

• struct literal expressions. we might then prohibit changing one of the parameter members of a "dependent struct" without updating the dependent members at the same time.
• verification of index bounds (suggests moving to a more robust verifier, such as Z3)
• propagation of values during unification (see sketch here: https://gist.github.com/kovach/bd75ae44abdabfdbf56b63ed918925ff )
• a <- b currently does not verify that overwriting a will not invalidate the computation of b (for instance, a[:,:] <- a*a generates incorrect code). the easiest immediate fix would be to always store b in a temp if it involves vectors.
• (a#b) <- c; -- this works when (a#b) is passed as an out variable, but is invalid (syntactically) in the given form
• polymorphism over base types, for instance: reverse {a, n} (x :: a[n]) :: a[n]

Warning-cleanliness

A thankless job: make the compiler -Wall-clean.

(^) typechecking

compiler bug (missing case) when ^ is applied to a matrix

recursive struct

this commit causes recursive struct definitions to loop during typechecking:
5db657d

fix, add unit test

Output Plover comments in generated C code

This seems useful for complex algorithms and for debugging the generated code (e.g. with the ARM gdb)

Documentation/Tutorial

Basic tutorial / syntax documentation

dependent structs

should be able to define something like

Struct {
  int n;
  double vec[n];
}

when generating struct code, might need upper limit for n for sizing

template haskell syntax?

look into
https://github.com/shayan-najd/MiniFeldspar
template haskell mechanism?

repl

make interpreter for Expr; write tests that compare generated output with haskell evaluation

libswiftnav reintegration

push parse branch into master
fix remaining cmake issues, use new plover compiler CLIi

Need explicit temporary variable for Vec

Works:

lol = seqList [
  FnDef "make_residual_measurements" (FnT [("n", IntType)] [
    ("Q", VecType [3,3] NumType),
    ("meas", VecType [3] NumType),
    ("resid", VecType [6] NumType)
  ] Void) $ seqList [
      "temp" := "Q" * "meas",
      "resid" :< "meas" :# "temp"
    ]
 ]

Doesn't work:

lol = seqList [
  FnDef "make_residual_measurements" (FnT [("n", IntType)] [
    ("Q", VecType [3,3] NumType),
    ("meas", VecType [3] NumType),
    ("resid", VecType [6] NumType)
  ] Void) $ seqList [
      "resid" :< "meas" :# ("Q" * "meas")
    ]
 ]

Error:

*** Exception: LOOK: Free (IntLit 3), Free (Ref "var1")

Maybe this is to be expected?

Better assignment checking

(x + x)[0] <- 22.0 should be caught by the compiler.

add output_c, output_h, include flags

also, support for multiple file arguments

figure out what compilation units really are

web interface

make a quick codemirror that sends expressions to ghci for evaluation

handle ghc warnings

refactor rules

need better organization to facilitate debugging
may also enable more general pattern matches, like a term within a context of a certain type

considering using a list of monad pattern matches (fail on match failure) or rules as objects

Terrifying error message from extra comma

 printf "\nCorrect solution to within %e!\n", tol;

yields

plover: compileStat not implemented: ((TupleLit' [((ConcreteApp' ((Get' (Ref (FnType (FnT [(Tag "examples/prelude.plv" (line 60, column 11) NoTag,"x$451$594$596",True,ArgIn,StringType)] (Just ArgIn) (IntType IDefault))) "printf"))) [((StrLit' "\nCorrect solution to within %e!\n"))] (IntType IDefault))),((Get' (Ref (FloatType FDefault) "tol$562")))]))

Removing the comma fixes it:

printf "\nCorrect solution to within %e!\n" tol;

We should do a better error message . . .

add horizontal concat operator for matrices

what should the syntax be?

No error on argument redefinition in body

This should give an error:

test = seqList [
  FnDef "test" (FnT [] [("x", NumType)] Void) $ seqList [
    "x" := 1
    ]
 ]

output:

void test(double x)
{
  double x;
  x = 1;
}

make tutorial

feature: Inlining data when possible

For model predictive control (and other applications), it is common to calculate a quadratic function as follows.

quad_cost {n, p, N}     -- For a horizon of N
  (P :: double[n, n])   -- Terminal cost
  (Q :: double[n, n])   -- Stage cost
  (R :: double[p, p])   -- Controller cost
  (x :: double[n, N])   -- N state vectors
  (u :: double[p, N-1]) -- (N-1) control vectors
  :: double
  := ( x[:, N]^T*P*x[:, N] +
       sum (vec k in N-1 -> x[:, k]^T*Q*x[:, k] + u[:, k]^T*R*u[:,k]);
     )[0];

In many cases, since we are not changing the matrices used in the quadratic function (either the matrices do not need to change or can't anyway because doing so would require a recompile), it is convenient to make functions where some of the inputs are prefilled in.

quad_cost_filled
  (x :: double[2, 2])
  (u :: double[2, 1]) :: double
  := quad_cost (mat (1, 0; 0, 1)) (mat (1, 0; 0, 1)) (mat (1, 0; 0, 1)) x u;

However, this version results in more assembly instructions (using gcc -O2) than the following, where the inlined data has been placed inside the quadratic function itself (loops can be unrolled, stack size can be constant, etc).

quad_cost2 -- For a horizon of 2
  (x :: double[2, 2])
  (u :: double[2, 1]) :: double
  := (
    P := (mat (1, 0; 0, 1));
    Q := (mat (1, 0; 0, 1));
    R := (mat (1, 0; 0, 1));
    N := 2;
    x[:, N]^T*P*x[:, N] +
       sum (vec k in N-1 -> x[:, k]^T*Q*x[:, k] + u[:, k]^T*R*u[:,k]);
     )[0];

When converted into assembly, quad_cost2 has 5x fewer instructions than quad_cost and it is possible to get rid of the loops.

It would be convenient if Plover had a way of simplifying any functions where some of the fields already contain constant data to help the C compiler later make more optimized versions of the code.

This could also probably be done if an inline tag existed that could be passed into the C code.

numeric simplification

partially evaluate numeric expressions uniformly across input term

assertions to create new type checking rules

e.g.

lol = seqList [
  FnDef "lol" (FnT [("a", IntType), ("b", IntType)] [
    ("va", VecType ["a"] NumType),
    ("vb", VecType ["b"] NumType)
    ] Void) $ seqList [
      assert $ "a" == 2 * "b",    -- Should allow the type checker to use the rule 
                                  -- a = 2b and insert an assertion into the generated C
      "va" := "vb" :# "vb"
    ]
 ]

module system

output module signature files, implement import statements

Random number functionality and matrix exponentials

@scottswift @peddie

Once I'm done with the hackathon I thought I might extend plover functionality for random numbers (could be useful for Monte Carlo tests).

1. sampling from normal distributions using Box-Muller (more efficient in comparison with rejection sampling)
2. sampling from discrete PDFs

Also the following (I have a C implementation sitting somewhere)

• Matrix exponential (using Pade approximations, like MATLAB does), c.f. "19 Dubious Ways..." http://epubs.siam.org/doi/abs/10.1137/S00361445024180

support compound matrix products

multiplication should support operand matrices whose elements are matrices

compiler errors are not verbose enough for debugging

keep track of current terms being reduced, or move to rewrite history log

link parser/compiler

missing/stale documentation

• Top-level Definitions
• Language Proposals
• overview of single index vectors, ^T,

tag output files

add comment with plover version hash, "machine generated" warning to outputs

block matrix simplification

• extend simplifier to matrices
• apply to assign_residual_obs_cov in amb_kf.c

language c quote for certain definitions?

like structs?

complex numbers

support C99 complex floating types

Assignment to concatenation

You should be able to assign to the concatenation of vectors.

x # y <- vec (22.0, 33.0, 44.0, 55.0)

generalized matrix layout

want to formalize concept of memory layout
want to dispatch unary/binary functions based on layout and algebraic rules
e.g. diagonal matrix * dense matrix, block matrix * block matrix

Main should print the help message if it fails.

unflatten compiler output

arithmetic, array indexing

QR least squares testing

figure out testing criterion
add unit tests to libswiftnav, pending #31

add hunit tests

PVT solver reintegration