HaRe-0.6: tools/Phugs/Phugs.hs
module Phugs where
----------------------------------------------------------------------
-- AST, etc.
----------------------------------------------------------------------
import Syntax hiding (E,P,D)
import PrettyPrint(pp)
type Name = String
data Op = Plus | Mult | IntEq | IntLess
data LS = Lazy | Strict deriving Eq
data P --- Nested Patterns
= Pconst Integer -- { 5 }
| Pvar Name -- { x }
| Ptuple [P] -- { (p1,p2) }
| Pcondata Name [P] -- data T1 = C1 t1 t2; {C1 p1 p1} = e
| Pnewdata Name P -- newtype T2 = C2 t1; {C2 p1} = e
| Ptilde P -- { ~p }
| Paspat Name P -- { x@p }
| Pwildcard -- { _ }
data E
= Var Name -- { x }
| Const Integer -- { 5 }
| App E E -- { f x }
| Abs [P] E -- { \ p1 p2 -> e }
| TupleExp [E] -- { (e1,e2) }
| ConApp Name [(E,LS)] -- data T1 = C1 t1 t2 \nl p = {C1 e1 e2}
| NewApp Name E -- newtype T2 = C2 t1 t2 \nl p = {C2 e1 e2}
| Seq E E -- { seq e1 e2 }
| Bin Op E E -- { e1 + e2 }
| Cond E E E -- { if e1 then e2 else e3 }
| Let [D] E -- { let x=e1 \nl y=e2 in e3 }
| Case E [Match] -- { case e of m1 \nl m2 }
| Undefined -- undefined
type Match =
(P, B, [D]) -- case e of { pat -> body where decs }
data D
= Fun Name [Clause] -- { f p1 p2 = b where decs }
| Val P B [D] -- { p = b where decs }
type Clause =
([P],B,[D]) -- f { p1 p2 = body where decs }
data B
= Guarded [(E,E)] -- f p { | e1 = e2 | e3 = e4 } where ds
| Normal E -- f p = { e } where ds
showB :: B -> String
showB (Normal e) = showE e
showB (Guarded ps) = foldr f "\n" ps
where f (e1,e2) ans = "| "++(showE e1) ++ " = " ++(showE e2)++ ans
showWhere ds = if null ds then "" else " where "
showD :: D -> String
showD (Val p body ds) = "VALDEF " ++ showP p ++ "=" ++ (showB body) ++ "\n" ++
(showWhere ds) ++ (showDs ds)
showD (Fun nm xs) = "FUNDEF "++ (foldr (++) "" (map f xs))
where f (ps,body,ds) =
nm ++ " " ++(showPs ps) ++ " = " ++(showB body) ++ "\n" ++
(showWhere ds) ++ (showDs ds)
showDs dcls = foldr (++) "" (map showD dcls)
showOp :: Op -> String
showOp Plus = "+"
showOp Mult = "*"
showOp IntEq = "=="
showOp IntLess = "<"
showP (Pconst i) = "LitPat("++show i++")"
showP (Pvar n) = "VarPat(\""++n++"\")"
showP (Pcondata n ns) = "ConstrPat(" ++ n ++ "," ++ (mkSlist ns) ++")"
showP (Paspat n p) = "AsPattern("++n++","++show p++")"
showP (Pnewdata n x) = error "no new constructor pattern yet"
showP (Ptilde p) = error "no tilde pattern yet"
showP (Ptuple ps) = "TuplePat(" ++ mkSlist ps ++ ")"
showP Pwildcard = "WildCard"
showPs [] = ""
showPs (p:ps) = (showP p)++" "++(showPs ps)
{- Pretty prints a haskell list expression into a stratego list -}
mkSlist = foldr
(\ s t -> if t/="Nil" then (show s++","++t) else (show s))
"Nil"
{- N.b., the resulting string is Stratego code -}
showE :: E -> String
showE (Var nm) = "HVar(\""++nm++"\")"
showE (Const i) = "HLit("++show i++")"
showE (App d d') = "HApp(" ++ showE d ++ "," ++ showE d' ++ ")"
showE (Abs p d) = "(\\" ++ (foldr (++) " " (map showP p)) ++ " -> "
++ showE d ++ ")"
showE (TupleExp l) = "(" ++
(foldr (\ s t ->
if t/="" then (showE s) ++ "," ++ t
else (showE s))
"" l)
++ ")"
showE (ConApp n l) = "(" ++ n ++ " " ++
(foldr (\ (s,ls) t ->
let sa = if (ls == Strict) then "!" else ""
in
if t/="" then sa ++ (showE s) ++ "," ++ t
else sa ++ (showE s))
"" l)
++ ")"
showE (NewApp n x) = "(" ++ n ++ " " ++ (showE x) ++ ")"
showE (Seq x y) = "(seq "++(showE x) ++ " " ++ (showE y) ++ ")"
showE (Bin op d d') = "(" ++ showE d ++ " " ++ showOp op ++ " " ++
showE d' ++ ")"
showE (Cond b e1 e2) = "if "++showE b++" then "++showE e1++" else "++show e2
showE (Let dcls d) = "let " ++
foldr (++) "" (map showD dcls)
++ " in " ++ showE d
showE (Case e ms) =
"(case " ++ showE e ++ " of " ++
(foldr (++) ""
(map (\ alt -> "[" ++ (showAlt alt) ++ "]") ms)) ++ ")"
where showAlt (p,b,ds) = show p ++ " -> " ++ show b ++ "\n" ++ showDs ds
instance Show D where
show = showD
instance Show E where
show = showE
instance Show P where
show = showP
instance Show B where
show = showB
-----------------------------------------------------------------------
bad x = error "not yet"
--translateP :: HsPat -> P
translateP (Pat p) =
case mapP translateP p of
HsPId n -> Pvar (showId n)
HsPLit (HsInt _ n) -> Pconst n
HsPInfixApp x op y -> Pcondata (show op) [x,y]
HsPApp n ps -> Pcondata (show n) ps
HsPTuple ps -> Ptuple ps
HsPIrrPat p -> Ptilde p
HsPParen p -> p
other -> error ("no "++(show other)++" patterns yet")
--translateD :: HsDecl -> D
translateD (d @ (Dec x)) =
case mapD translateE translateP (map translateD) bad bad bad x of
HsPatBind loc p b ds -> Val p (translateRhs b) ds
HsFunBind loc matches -> Fun (name matches) (map g matches)
where name ((HsMatch loc nm ps rhs ds): ms) = (showId (HsVar nm))
g (HsMatch loc nm ps rhs ds) = (ps,translateRhs rhs,ds)
other -> error ("illegal dec "++(show d))
--translateRhs :: HsRhs E -> B
translateRhs (HsBody e) = Normal e
translateRhs (HsGuard triples) = Guarded(map f triples)
where f (loc,guard,body) = (guard,body)
--translateAlt :: HsAlt E P [D] -> (P,B,[D])
translateAlt (HsAlt loc pat rhs ds) = (pat,translateRhs rhs,ds)
--translateE :: HsExp -> E
translateE (e @ (Exp x)) =
case mapE translateE translateP (map translateD) bad bad x of
HsId n -> Var (showId n)
HsApp x y -> App x y
HsLit (HsInt _ n) -> Const n
HsInfixApp x op z -> App (App (Var (showId op)) x) z
HsNegApp _ x -> App (Var "negate") x
HsLambda ps e -> Abs ps e
HsLet ds e -> Let ds e
HsIf x y z -> Cond x y z
HsCase e alts -> Case e (map translateAlt alts)
HsTuple xs -> TupleExp xs
HsList xs -> f xs
where f [] = ConApp "[]" []
f (x:xs) = ConApp ":" [(x,Lazy),(f xs,Lazy)]
HsParen x -> x
HsLeftSection x op -> Abs[Pvar "zzz"] (App (App (Var (show op)) x)
(Var "zzz"))
HsRightSection op y -> Abs[Pvar "zzz"] (App (App (Var (show op))
(Var "zzz")) y)
other -> error ("no translation yet for: "++(show e))
--showId (HsVar x) = show x
--showId (HsCon x) = show x
showId x = pp x
----------------------------------------------------------------------
-- Values
----------------------------------------------------------------------
data V
= Z Integer --- scalars
| FV (V -> V) --- functions
| Tagged Name [V] --- algebraic structured data
| TV [V] --- tuple values
-------------------------------------------------------------
-------------------------------------------------------------
type Env = Name -> V -- Maps Names to Values V
xEnv :: Env -> [Name] -> [V] -> Env
xEnv rho (x:xs) (b:bs) = (xEnv (tweek rho x b) xs bs)
where tweek f x y = \ z -> if x == z then y else f z
xEnv rho [] [] = rho
------------------------------------------------------------------
{-
There are variables in a pattern p with the appropriate types corresponding
to the range of this function x1::b1, ..., xn::bn.
Call these variables the "fringe" of p. (fringe p) returns the free
variables of p in *order* of occurrence from left to right. -}
-- returns the fringe of p in order from left to right.
fringe :: P -> [Name]
fringe (Pconst i) = []
fringe (Pvar x) = [x]
fringe (Pcondata n ps) = foldr (++) [] (map fringe ps)
fringe (Ptilde p) = fringe p
fringe (Ptuple ps)= foldr (++) [] (map fringe ps)
fringe (Paspat n p) = n : (fringe p)
fringe Pwildcard = []
data Predicate = Univ | Strong Predicate | List [Predicate]
| TCongruence Name [Predicate] deriving Show
patPred :: P -> [(Name,Predicate)] -> Bool -> (Predicate,Bool)
patPred (Pvar x) sigma b = (purify $ lookup x sigma, is_strong (purify $ lookup x sigma))
where
is_strong (Strong _) = True
is_strong _ = False
--xb = purify $ lookup x sigma
patPred Pwildcard sigma b = (Univ,False)
patPred (Ptilde p) sigma b = patPred p sigma False
patPred (Pcondata n ps) sigma b =
let (List preds, s) = map_patPred ps sigma b
in
if (s || b) then
(Strong (TCongruence n preds), True)
else (Univ, False)
map_patPred :: [P] -> [(Name,Predicate)] -> Bool -> (Predicate,Bool)
map_patPred [] sigma b = (List [], False)
map_patPred (p:ps) sigma b = (List (pp:pps), s1 || s2)
where
(pp,s1) = patPred p sigma b
(List pps,s2) = map_patPred ps sigma b
pat2pred :: P -> [Predicate] -> Predicate
pat2pred p plist = fst (patPred p (zip (fringe p) plist) True)
frD :: [D] -> [Name]
frD [] = []
frD ((Fun f _):ds) = f : (frD ds)
frD ((Val p _ _):ds) = fringe p ++ (frD ds)
--- This collects the function names & patterns from declarations
--- as a single tuple pattern
declared :: [D] -> P
declared ds = ptuple $ map getbinder ds
where
getbinder (Fun f _) = Pvar f
getbinder (Val p _ _) = tildefy p
arity (Pvar x) = 1
arity (Ptuple ps) = sum(map arity ps)
arity (Pcondata n ps) = sum(map arity ps)
arity (Ptilde p) = arity p
tuple :: [V] -> V
tuple [v] = v
tuple vs = TV vs
tagtuple :: [V] -> V
tagtuple [v] = v
tagtuple vs = Tagged "tuple" vs
ptuple :: [P] -> P
ptuple [p] = p
ptuple ps = Pcondata "tuple" ps
tildefy :: P -> P
tildefy p = case p of
(Ptilde p') -> p
(Pvar x) -> p
_ -> (Ptilde p)
-------------------------------------------
-- Important Semantic Operators --
-------------------------------------------
-- Composition operators (N.b., both diagrammatic order.)
(>>>) :: (a -> b) -> (b -> c) -> a -> c
f >>> g = g . f -- Functional
(<>) :: (a -> Maybe b) -> (b -> Maybe c) -> a -> Maybe c
f <> g = \x -> f x >>= g -- Kleisli
bottom :: a -- domains are pointed
bottom = undefined
purify :: Maybe a -> a -- "run" of Maybe monad
purify (Just x) = x
purify Nothing = bottom
fix :: (a -> a) -> a -- least fixed point
fix f = f (fix f)
semseq :: V -> V -> V
semseq x y = case x of
(Z _) -> y ;
(FV _) -> y ;
(Tagged _ _) -> y ;
(TV _) -> y
sharp :: Int -> [V] -> (V -> V) -> V -- Currying
sharp 0 vs beta = beta (tuple vs)
sharp n vs beta = FV $ \ v -> sharp (n-1) (vs++[v]) beta
app :: V -> V -> V -- Application
app (FV f) x = f x
fatbar :: (a -> Maybe b) -> (a -> Maybe b) -> (a -> Maybe b)
f `fatbar` g = \ x -> (f x) `fb` (g x)
where
fb :: Maybe a -> Maybe a -> Maybe a
Nothing `fb` y = y
(Just v) `fb` y = (Just v)
{- The function match is used to construct the meaning of a Match. -}
match :: Env -> (P, B, [D]) -> V -> Maybe V
match rho (p,b,ds) = mP p <> (\vs -> mwhere (xEnv rho xs vs) b ds)
where xs = fringe p
-- used in letbind and mE
lam :: P -> E -> Env -> V -> V
lam p e rho = (mP p <> ((\vs -> mE e (xEnv rho xs vs)) >>> Just)) >>> purify
where xs = fringe p
mcase :: Env -> [Match] -> V -> V
mcase rho ml = (fatbarL $ map (match rho) ml) >>> purify
where fatbarL :: [V -> Maybe V] -> V -> Maybe V
fatbarL ms = foldr fatbar (\ _ -> (Just bottom)) ms
{-
(letbind rho ds e) is the meaning of Haskell's mutually recursive
let construct. Its definition uses a standard technique for
defining mutual recursion with explicit fix-points:
let p1 = e1
...
pn = en === (\(p1,...,pn) -> e) (fix \(~p1,...,~pn) -> (e1,...,en))
in
e
In order for the fixpoint to be defined, each pattern pi in the argument
to fix is "~"-ed, so that the function is lazy.
-}
letbind :: Env -> [D] -> E -> V
letbind rho [] e = mE e rho
letbind rho ds e = (lam dp e rho) v
where
dp = tildefy $ declared ds
xs = frD ds
decls env = tagtuple $ map (\d -> mD d env) ds
v = fix $ ((mP dp) <>
((\vs -> decls (xEnv rho xs vs)) >>> Just)) >>> purify
mwhere :: Env -> B -> [D] -> Maybe V
mwhere rho b [] = mB b rho
mwhere rho b ds = (wherecls dp b rho) v
where
wherecls p b rho = (mP p <> (\vs -> mB b (xEnv rho xs vs)))
where xs = fringe p
dp = tildefy $ declared ds
xs = frD ds
decls env = tagtuple $ map (\d -> mD d env) ds
v = fix $ ((mP dp) <>
((\vs -> decls (xEnv rho xs vs)) >>> Just)) >>> purify
{-
Translation of function bindings from Haskell98 Report (p. 54):
x p(1,1) ... p(1,k) match1
...
x p(n,1) ... p(n,k) matchn
is equivalent to
x = \x1 ... xn -> case (x1,...,xn) of
(p(1,1),...,p(1,k)) -> match1
...
(p(n,1),...,p(n,k)) -> matchn
where x1,...,xn are fresh variables.
The function below, "mD", is constructed similarly, although without any
variable generation.
-}
--------------------------------------------
--- semantic functions ---
--------------------------------------------
mE :: E -> Env -> V
mP :: P -> V -> Maybe [V]
mB :: B -> Env -> Maybe V
mD :: D -> Env -> V
phugs ds = mE (Let ds (Var "topLevel")) rho0
--(App (Var "odd") (Const 3))
rho0 = xEnv rhoNull ["==","-","*","True","False"] [eqZ,minusZ,multZ,tt,ff]
where rhoNull = \msg -> (error ("You're applying the empty env to:"++msg))
eqZ = FV $ \ (Z i) -> (FV $ \ (Z j) ->
if i==j then (Tagged "True" [])
else (Tagged "False" []))
minusZ = FV $ \ (Z i) -> (FV $ \ (Z j) -> (Z $ i-j))
multZ = FV $ \ (Z i) -> (FV $ \ (Z j) -> (Z $ i*j))
tt = Tagged "True" []
ff = Tagged "False" []
-----------------------------------------------------------------
-- The meaning of expressions
-----------------------------------------------------------------
ifV :: V -> a -> a -> a
ifV (Tagged "True" []) x y = x
ifV (Tagged "False" []) x y = y
mE (Var n) rho = rho n
mE (Const i) rho = (Z i)
mE (TupleExp es) rho = TV $ map (\e-> mE e rho) es
mE (Cond e0 e1 e2) rho = ifV (mE e0 rho) (mE e1 rho) (mE e2 rho)
mE (App e1 e2) rho = app (mE e1 rho) (mE e2 rho)
mE (Abs [p] e) rho = FV $ lam p e rho
mE (Abs ps e) rho = mE (foldr (\p -> \body -> Abs [p] body) e ps) rho
mE (Let ds e) rho = letbind rho ds e
mE (Case e ml) rho = mcase rho ml (mE e rho)
mE (ConApp n el) rho = evalL el rho n []
where evalL :: [(E,LS)] -> Env -> Name -> [V] -> V
evalL [] rho n vs = Tagged n vs
evalL ((e,Strict):es) rho n vs = semseq (mE e rho)
(evalL es rho n (vs ++ [mE e rho]))
evalL ((e,Lazy):es) rho n vs = evalL es rho n (vs ++ [mE e rho])
mE (NewApp n e) rho = mE e rho
mE Undefined rho = bottom
mE (Seq e1 e2) rho = semseq (mE e1 rho) (mE e2 rho)
mE (Bin op e1 e2) rho = binOp op (mE e1 rho) (mE e2 rho)
where binOp Plus (Z i) (Z j) = Z $ i+j
binOp Mult (Z i) (Z j) = Z $ i*j
binOp IntEq (Z i) (Z j) = Tagged (equal i j) []
binOp IntLess (Z i) (Z j) = Tagged (less i j) []
equal i j = if i==j then "True" else "False"
less i j = if i<j then "True" else "False"
mB (Normal e) rho = Just (mE e rho)
mB (Guarded gl) rho = ite gl rho
where ite [] rho = Nothing
ite ((g,e):gs) rho = ifV (mE g rho) (Just (mE e rho)) (ite gs rho)
{-
A pattern p may be viewed as a function of type ::a -> Maybe (b1,...,bn).
The denotation of a pattern is represented here as a function ::V -> Maybe [V].
-}
mP (Pvar x) v = Just [v]
mP (Pconst i) (Z j) = if i==j then Just [] else Nothing
mP (Ptuple ps) (TV vs) = stuple (map mP ps) vs
mP (Pcondata n ps) (Tagged t vs) = if n==t then
stuple (map mP ps) vs
else Nothing
mP (Pnewdata n p) v = mP p v
mP (Ptilde p) v = Just(case mP p v of
Nothing -> replicate (arity p) bottom
Just z -> z)
mP Pwildcard v = Just []
stuple :: [V -> Maybe [V]] -> [V] -> Maybe [V]
stuple [] [] = Just []
stuple (q:qs) (v:vs) = do v' <- q v
vs' <- stuple qs vs
Just (v'++vs')
mD (Fun f cs) rho = sharp lps [] body
where
body = mcase rho (map (\(ps,b,ds) -> (ptuple ps, b,ds)) cs)
lps = length ((\(pl,_,_)->pl) (head cs))
mD (Val p b ds) rho = purify $ mwhere rho b ds
--grunt (Val p b ds) rho
--grunt (Val p b ds) rho = fix $ match rho (tildefy p,b,ds) >>> purify
showV :: V -> String
showV (Z i) = show i
showV (FV _) = "(function value)"
showV (Tagged n []) = n
showV (Tagged n [v]) = "("++n++" ?)"
showV (Tagged n [v1,v2]) = "("++n++" "++show v1++" "++show v2++")"
showV (TV []) = "()"
showV (TV [v]) = "("++show v++")"
showV (TV [v1,v2]) = "("++show v1++","++show v2 ++")"
instance Show V where
show = showV
{-
rho0 = (\msg -> error "hey - you're applying the empty env!")
go e = mE e rho0
-}
omegafac n = let fac x = if x==0 then 1 else x * (fac (x-1)) in fac n
omega :: V
omega = case (fix (\ i -> i) (Z 9)) of
FV f -> FV f
omega1 :: Integer -> (Integer -> Integer) -> Integer -> Integer
omega1 x f = if x==0 then f else (omega1 (x-1) f)