[<<][meta][>>][..]

Pfff...

This local reasoning isn't getting me very far.  Suddenly I run into
the need for a "Cons" in the Term language.

Or maybe it is.  Makes sense at least since it solves another problem:
how to get to a list of Var types for App?  Like this:

instance Pair Code where
  cons (Code a, Code b) = Code $ Cons a b
  uncons (Code (Cons a b)) = (Code a, Code b)
  
instance Loop MCode' Code where
  _app rf ras = app rf (pack ras) where
    app :: Code (as -> MCode t) -> Code as -> MCode (Code t)
    app (Code (FRef f)) (Code as) = 
      return $ Code $ App f (toList as) where
        -- Convert the "Cons" structure to a flat list of variables.
        toList (Cons a b) = toList a ++ toList b
        toList (Ref v) = [v]

Next: Lambda.

The whole point is that termFun will take functions like this:

  (Code a, Code b) -> MCode (Code c, Code d)

so why can't I feed a host embedding straight into termFun?  At this
point we changed completely from r (a,b) to (r a, r b).

It seems to be that this is just what is needed:

  _lambda f = Code $ termFun f

With some extra instances:

instance Args Code as ras => CompileData ras Term
instance Args Code as ras => CompileVar ras



[Reply][About]
[<<][meta][>>][..]