content: 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)
  			
  