***********************************************************************
* A Continuation Semantics for the Eager Functional Language          *
* from Chapter 12 of Reynolds, including calcc and throw.             *
***********************************************************************

Written by Paul Hudak.

> module EagerFL where

SYNTAX
======

Some type synonyms to use Reynolds names:

> type NatConst  = Int		-- but should not include negative numbers
> type BoolConst = Bool
> type Tag       = NatConst

> data Exp = 
> -- constants:
>     NatConst NatConst		-- integer literals
>   | BoolConst BoolConst	-- booleans
>   | Nil			-- nil
> -- arithmetic:
>   | Neg Exp			-- negation
>   | Exp :+: Exp		-- addition
>   | Exp :-: Exp		-- subtraction
>   | Exp :*: Exp		-- multiplication
>   | Exp :/: Exp		-- division
>   | Exp `Rem` Exp		-- remainder
> -- relational operators:
>   | Exp :=:  Exp		-- equality
>   | Exp :/=: Exp		-- inequality
>   | Exp :<:  Exp		-- less than
>   | Exp :<=: Exp		-- less than or equal
>   | Exp :>:  Exp		-- greater than
>   | Exp :>=: Exp		-- greater than or equal
> -- logical operators:
>   | Not Exp			-- negation
>   | Exp :/\:  Exp		-- conjunction (and)
>   | Exp :\/:  Exp		-- disjunction (or)
>   | Exp :=>:  Exp		-- implication
>   | Exp :<=>: Exp		-- if and only if
> -- conditional:
>   | If Exp Exp Exp            -- conditional
> -- variables, lambdas, and applications:
>   | Var Var			-- variables
>   | App Exp Exp		-- applications
>   | Lam Pat Exp		-- functions with pattern arguments
> -- tuples:
>   | Tup [Exp]			-- tuples
>   | Prj Exp Tag		-- tuple projection
> -- sums:
>   | Sum Tag Exp		-- sums (i.e. alternatives; tagged values)
>   | SumCase Exp [Exp]		-- sum discrimination (i.e. case)
> -- errors:
>   | Error			-- run-time error
>   | TypeError			-- type error
> -- binding forms:
>   | Let    [(Pat,Exp)] Exp	-- let expression
>   | LetRec [(Var,Pat,Exp)] Exp-- recursive let expression
> -- callcc and throw:
>   | CallCC Exp
>   | Throw Exp Exp
>   deriving (Eq, Show)
>
> data Pat = Pat1 Var
>          | Pat2 [Pat]
>   deriving (Eq, Show)

Variables are just strings:

> type Var = String

FIXITIES
========

> infixl 9 :*:, :/:, `Rem`
> infixl 8 :-:, :+:
> infix  7 :=:, :/=:, :<:, :>:, :<=:, :>=:
> infixl 6 :/\:
> infixl 5 :\/:
> infixr 4 :=>:
> infixr 3 :<=>:

SEMANTIC DOMAINS
================

> data VStar = Norm V
>            | Err  Err
>      deriving (Eq,Show)
>
> data Err   = DynErr
>            | TypErr
>      deriving (Eq,Show)
>
> data V     = VInt  Int
>            | VBool Bool
>            | VNil
>            | VTup  [V]
>            | VSum  (Int, V)
>            | VFun  (V -> VCont -> VStar)
>            | VCont VCont
>      deriving (Eq,Show)
>
> type VCont = V -> VStar
>
> instance Show (V -> VCont -> VStar) where
>   show f = "[Function]"
> 
> instance Show VCont where
>   show f = "[Function]"
>
> instance Eq VCont where
>   f == g  =  False
>
> instance Eq (V -> VCont -> VStar) where
>   f == g  =  False
>
> err   = Err  DynErr
> tyerr = Err  TypErr
> nil   =      VNil

AUXILIARY FUNCTIONS 
===================

Projections:

> i_norm = Norm
>
> i_int  = VInt
> i_bool = VBool
> i_tup  = VTup
> i_alt  = VSum
> i_fun  = VFun
> i_cont = VCont

Type checking:

> int ::  (Int -> VStar) -> (V -> VStar)
> f `int`  VInt i  = f i
> f `int`  _       = tyerr
>
> bool :: (Bool -> VStar) -> (V -> VStar)
> f `bool` VBool b = f b
> f `bool` _       = tyerr
>
> tup ::  ([V] -> VStar) -> (V -> VStar)
> f `tup` VTup ts  = f ts
> f `tup` _        = tyerr
>
> alt ::  ((Int,V) -> VStar) -> (V -> VStar)
> f `alt`  VSum s  = f s
> f `alt`  _       = tyerr
>
> fun ::  ((V->VCont->VStar) -> VStar) -> (V -> VStar)
> f `fun`  VFun g  = f g
> f `fun`  _       = tyerr
>
> cont ::  (VCont -> VStar) -> (V -> VStar)
> f `cont` VCont g = f g
> f `cont` _       = tyerr

So (f `int`) or (int f) is equivalent to f_int in Reynolds.

ENVIRONMENTS
============

> type E = Var -> V
>
> extend :: E -> Var -> V -> E
> extend e v i v' = if v == v' then i else e v'

So "extend s v i" is equivalent to "s [v:i]" in Reynolds.

> emptyE x = error ("Unbound variable: " ++ x)

Syntax Expansion
================

An infinite supply of fresh variabes, using the convention that no
variable name in the program begins with "_":

> names = map (("_"++).show) [0..]

SEMANTICS
=========

The key semantic function:

> meaning :: Exp -> E -> VCont -> VStar
> meaning = mean . desugar

After desugaring:

> mean :: Exp -> E -> VCont -> VStar
> -- constants:
> mean Nil           eta k = k nil
> mean Error         eta k = err
> mean TypeError     eta k = tyerr
> mean (NatConst n)  eta k = k (i_int n)
> mean (BoolConst b) eta k = k (i_bool b)
>
> -- unops:
> mean (Neg e) eta k = mean e eta $ int  $ \i -> k (i_int  (-i))
> mean (Not e) eta k = mean e eta $ bool $ \b -> k (i_bool (not b))
>
> -- binops:
> mean (e :+:  e')  eta k = binop i_int  int  (+)  e e' eta k
> mean (e :-:  e')  eta k = binop i_int  int  (-)  e e' eta k
> mean (e :*:  e')  eta k = binop i_int  int  (*)  e e' eta k
> mean (e :/=: e')  eta k = binop i_bool int  (/=) e e' eta k
> mean (e :<:  e')  eta k = binop i_bool int  (<)  e e' eta k
> mean (e :>:  e')  eta k = binop i_bool int  (>)  e e' eta k
> mean (e :<=: e')  eta k = binop i_bool int  (<=) e e' eta k
> mean (e :>=: e')  eta k = binop i_bool int  (>=) e e' eta k
> mean (e :/\: e')  eta k = binop i_bool bool (&&) e e' eta k
> mean (e :\/: e')  eta k = binop i_bool bool (||) e e' eta k
> mean (e :=>: e')  eta k = binop i_bool bool  f   e e' eta k
>   where f b b' = if b then b' else True   -- not b || b'
> mean (e :<=>: e') eta k = binop i_bool bool  f   e e' eta k
>   where f b b' = if b then b' else not b' -- (b&&b')||(not (b||b'))
>
> -- equality:
> mean (e :=: e')  eta k =
>   mean e  eta $ \i  ->
>   mean e' eta $ \i' -> k (i_bool (i==i'))
>
> -- division and remainder:
> mean (e :/: e') eta k =
>   mean e  eta $ int $ \i  ->
>   mean e' eta $ int $ \i' -> 
>     if i'==0 then err else k (i_int (i `div` i'))
>
> mean (e `Rem` e') eta k =
>   mean e  eta $ int $ \i  ->
>   mean e' eta $ int $ \i' -> 
>     if i'==0 then err else k (i_int (i `rem` i'))
>
> -- conditional
> mean (If b c a) eta k =
>   mean b eta $ bool $ \b -> 
>     if b then mean c eta k else mean a eta k
>
> -- vars, apps, and lambdas:
> mean (Var v) eta k = k (eta v)
>
> mean (App e e') eta k =
>   mean e  eta $ fun $ \f ->
>   mean e' eta $       \x -> f x k
>
> mean (Lam (Pat1  v) e) eta k =
>   k (i_fun (\z k' -> mean e (extend eta v z) k'))
> mean (Lam (Pat2 ps) e) eta k = 
>   error "Lambda patterns should be desugared."
>
> -- tuples
> mean (Tup es) eta k = tupm es []
>   where tupm []     zs = k (i_tup (reverse zs))
>         tupm (e:es) zs = mean e eta $ \z -> tupm es (z:zs)
>
> mean (Prj e n) eta k =
>   mean e eta $ tup $ \ts -> 
>     if n < length ts then k (ts!!n)
>                      else tyerr

mean e eta $ tup $ \ts ->
mean n eta $ int $ \i  ->
     if i > 0 && i < length ts then k (ts!!i)
                      else tyerr

> -- sums:
> mean (Sum n e) eta k =
>   mean e eta $ \z -> k (i_alt (n,z))
>
> mean (SumCase e fs) eta k =
>   mean e eta $ alt $ \(n,z) ->
>     if n < length fs 
>     then mean (fs!!n) eta $ fun $ \f -> f z k
>     else tyerr
>
> -- let expression:
> mean (Let eqns e) eta k = error "Let expression should be desugared."
>
> -- recursive let:
> mean (LetRec eqns e) eta k = 
>   let eta' = foldr f eta eqns
>       f (v,Pat1 u,e) eta = extend eta v 
>                              (i_fun (\z -> mean e (extend eta' u z)))
>   in mean e eta' k
>
> -- callcc and throw
> mean (CallCC e) eta k = 
>   mean e eta $ fun $ \f -> f (i_cont k) k
>
> mean (Throw e e') eta k =
>   mean e eta $ cont $ \k' -> mean e' eta k'


Auxilliary function for strict binary operators:

> binop inj tc op e e' eta k =
>   meaning e  eta $ tc $ \i  -> 
>   meaning e' eta $ tc $ \i' -> k (inj (i `op` i'))

DESUGARING
==========

Top-level desugaring:

> desugar :: Exp -> Exp
> desugar e = desug e [] names

Main desugaring function:

> desug :: Exp -> [(Var,Exp)] -> [Var] -> Exp
> -- constants:
> desug Nil           as vs = Nil
> desug Error         as vs = Error
> desug TypeError     as vs = TypeError
> desug (NatConst k)  as vs = NatConst k
> desug (BoolConst b) as vs = BoolConst b
>
> -- unops:
> desug (Neg e) as vs   = Neg (desug e as vs)
> desug (Not e) as vs   = Not (desug e as vs)
> desug (Prj e k) as vs = Prj (desug e as vs) k
> desug (Sum k e) as vs = Sum k (desug e as vs)
>
> -- binops:
> desug (e :+:   e') as vs = bDesug e e' (:+:)  as vs
> desug (e :-:   e') as vs = bDesug e e' (:-:)  as vs
> desug (e :*:   e') as vs = bDesug e e' (:*:)  as vs
> desug (e :=:   e') as vs = bDesug e e' (:=:)  as vs
> desug (e :/=:  e') as vs = bDesug e e' (:/=:) as vs
> desug (e :<:   e') as vs = bDesug e e' (:<:)  as vs
> desug (e :>:   e') as vs = bDesug e e' (:>:)  as vs
> desug (e :<=:  e') as vs = bDesug e e' (:<=:) as vs
> desug (e :>=:  e') as vs = bDesug e e' (:>=:) as vs
> desug (e :/\:  e') as vs = bDesug e e' (:/\:) as vs
> desug (e :\/:  e') as vs = bDesug e e' (:\/:) as vs
> desug (e :=>:  e') as vs = bDesug e e' (:=>:) as vs
> desug (e :<=>: e') as vs = bDesug e e' (:<=>:)as vs
> desug (e :/:   e') as vs = bDesug e e' (:/:)  as vs
> desug (e `Rem` e') as vs = bDesug e e'  Rem   as vs
> desug (App  e  e') as vs = bDesug e e'  App   as vs
>
> -- ternary op:
> desug (If b c a) as vs =
>   If (desug b as vs) (desug c as vs) (desug a as vs)
>
> -- n-ary ops:
> desug (Tup es)       as vs = 
>   Tup (map (\e -> desug e as vs) es)
> desug (SumCase e fs) as vs = 
>   SumCase (desug e as vs) (map (\e -> desug e as vs) fs)
>
> -- variables:
> desug (Var v) as vs = lookUp v as
>
> -- lambda:
> desug (Lam (Pat1  v) e) as    vs  = Lam (Pat1 v) (desug e as vs)
> desug (Lam (Pat2 ps) e) as (v:vs) =
>   let as' = depat ps (Var v) 0
>   in Lam (Pat1 v) (desug e (as'++as) vs)
>
> -- let expression:
> desug (Let eqns exp) as vs = 
>   desug (expand eqns) as vs
>   where expand  []          = exp
>         expand ((p,e):eqns) = App (Lam p (expand eqns)) e
>
> -- recursive let:
> desug (LetRec eqns e) as vs =
>   LetRec (map f eqns) (desug e as vs)
>   where f (v,p,e) =
>              let Lam p' e' = desug (Lam p e) as vs
>              in (v,p',e')
>
> -- callcc and throw:
> desug (CallCC e) as vs = CallCC (desug e as vs)
> desug (Throw e e') as vs = Throw (desug e as vs) (desug e' as vs)


Auxilary functions for desugaring:

Binary operators:

> bDesug e1 e2 op as vs = desug e1 as vs `op` desug e2 as vs

Variable lookup:

> lookUp v as = case lookup v as of
>                 Just e  -> e
>                 Nothing -> Var v
>                         -- error ("Unknown variable: " ++ v)

Compiling patterns:

> depat []     e n = []
> depat (p:ps) e n = dep1 p e n ++ depat ps e (n+1)

> dep1 (Pat1 v)  e n = [(v, Prj e n)]
> dep1 (Pat2 ps) e n = depat ps (Prj e n) 0

TESTS
=====

> tpats = [Pat1 "a", Pat2 [Pat1 "b", Pat1 "c"], Pat1 "d"]
> t1 = depat tpats (Var "v") 0

t1 ==> [("a", Prj (Var "v") 0),
        ("b", Prj (Prj (Var "v") 1) 0),
        ("c", Prj (Prj (Var "v") 1) 1),
        ("d", Prj (Var "v") 2)]

> tlam = Lam (Pat2 tpats) (Var "b" :+: Var "d")
> t2 = desugar tlam

t2 ==> Lam (Pat1 "v0") (Prj (Prj (Var "v0") 1) 0 :+: Prj (Var "v0") 2)

Complete programs:
------------------

> test p = meaning p emptyE i_norm

Factorial:

> p1 = LetRec [("fac", Pat1 "n", 
>               If (Var "n" :=: NatConst 0)
>                  (NatConst 1)
>                  (Var "n" :*: App (Var "fac") (Var "n" :-: NatConst 1))
>              )]
>        (App (Var "fac") (NatConst 5))

test p1 ==> Norm (VInt 120)

Lists:

> listFns = [(Pat1 "cons",
>            Lam (Pat2 [Pat1 "x", Pat1 "xs"]) (Tup [Var "x", Var "xs"])),
>           (Pat1 "car",
>            Lam (Pat1 "xs") (Prj (Var "xs") 0)),
>           (Pat1 "cdr",
>            Lam (Pat1 "xs") (Prj (Var "xs") 1)),
>           (Pat1 "null",
>            Lam (Pat1 "xs") (Var "xs" :=: Nil))]

> alist = [(Pat1 "l1",
>           App (Var "cons") 
>               (Tup [NatConst 1,
>                     (App (Var "cons")
>                          (Tup [NatConst 2, Nil]))]))]

> p2 = Let (listFns++alist)
>          (App (Var "cdr") (Var "l1"))

test p2 ==> Norm (VTup [VInt 2,VNil])

These are from Reynolds: reduce (fold) and append (defined using reduce):

> red = ("reduce",
>        Pat2 [Pat1 "x", Pat1 "f", Pat1 "a"],
>        If (App (Var "null") (Var "x"))
>           (Var "a")
>           (App (App (Var "f") (App (Var "car") (Var "x")))
>                (App (Var "reduce") (Tup [App (Var "cdr") (Var "x"),
>                                          Var "f",
>                                          Var "a"]))))

> app = (Pat1 "append",
>        Lam (Pat2 [Pat1 "x", Pat1 "y"])
>            (App (Var "reduce")
>                 (Tup [Var "x",
>                       Lam (Pat1 "i")
>                           (Lam (Pat1 "z")
>                                (App (Var "cons") 
>                                     (Tup [Var "i",Var "z"]))),
>                       Var "y"])))

Test of append:

> p3 = Let (listFns++alist)
>          (LetRec [red]
>                  (Let [app]
>                       (App (Var "append")
>                            (Tup [Var "l1", Var "l1"]))))

test p3 ==> Norm (VTup [VInt 1,VTup [VInt 2,VTup [VInt 1,VTup [VInt 2,VNil]]]])

Simple callcc/throw example from Reynolds:

> p4 = CallCC (Lam (Pat1 "k") 
>                  (NatConst 2 :+: Throw (Var "k") 
>                                        (NatConst 3 :*: NatConst 4)))