Sun Oct 16 09:54:38 EDT 2011

TML + SysM

Time to integrate the insights from TML into SysM.  Most important
problem: how to deal with the existentials.

How does genFun work on something that's been hidden behind SysM with
an existential state qualifier?

Let's see how to go about this.  First, the genFun (which needs a
different name btw; i'm aliasing it to `compile'.) needs to be changed
to support a more generic interface.  Instead of only working on Code
deconstruction (:: Code t -> Term) that operation should be made
generic as "compilable" much like the PrimData class is expressing.

Let's try: Compile.hs

It seems to at least typecheck, so now I need some better names to
reflect the meaning behind this:

class CompData r s | r -> s where
  compile :: r -> s
  var     :: VarName -> r

class CompFun s m f | f -> m, f -> s where
  codeApp :: [VarName] -> f -> ([s], m [s])

CompData means compilable data: convert representation r to syntax (data) s.

CompFun means compilable function: convert function and variable name
pool to a pair of inputs and outputs parameterized by some monad.