-- Terms with binary operators and scoped variable definitions

data Term a b c = Lit a | Var c | Bop b (Term a b c) (Term a b c)
                | Let c (Term a b c) (Term a b c) deriving Show

fold f g h k (Lit a)     = f a
fold f g h k (Bop o l r) = g o (fold f g h k l) (fold f g h k r)
fold f g h k (Let x d t) = h x (fold f g h k d) (fold f g h k t)
fold f g h k (Var x)     = k x


-- Binary operators and semantics for arithmetic

data Oper = Plus | Mult | Diff deriving Show

syn Plus = "+" ;  syn Mult = "*" ;  syn Diff = "-"
sem Plus = (+) ;  sem Mult = (*) ;  sem Diff = (-)


-- Variables and environments

data Id = X | Y | Z deriving (Ord, Eq, Enum)

prv X = "x"; prv Y = "y"; prv Z = "z"

set env x v = \y -> if x==y then v else env y

empty = \x -> undefined


-- Evaluation and environments

eval (Lit a)     env = a
eval (Bop o l r) env = sem o (eval l env) (eval r env)
eval (Let x d t) env = eval t (set env x (eval d env))
eval (Var x)     env = env x


-- Evaluation as a "higher-order" fold

fval :: Eq c => Term Integer Oper c -> (c -> Integer) -> Integer

fval = fold (\a     -> (\env ->  a ))
            (\o l r -> (\env ->  sem o (l env) (r env) ))
            (\x d t -> (\env ->  t (set env x (d env)) ))
            (\x     -> (\env ->  env x ))


-- Pretty-printing

prdef x d t = par $ unwords ["let",x,"=",d,"in",t]

prtm :: Term Integer Oper Id -> String
prtm = fold show (fmt . syn) (prdef . prv) prv

fmt o l r = par $ unwords [l,o,r]

par s = "(" ++ s ++ ")"


-- Tracing: fold producing a function from envs to traces

trace :: Eq c => Term Integer Oper c -> (c -> Integer) -> [Term Integer Oper c]
trace = fold (\a     e -> [Lit a])
             (\o l r e -> comb o (l e) (r e))
             (\x d t e -> let de@(v:_) = d e in
                          defn x de (t (set e x (eval v e))))
             (\x     e -> [Lit (e x), Var x])

comb op ls@(Lit l:_) (Lit r:tr) = let (&) = Bop op in
  Lit (sem op l r) : [x & Lit r | x<-ls] ++ [last ls & y | y<-tr]
comb op (a:_) (b:_) = [] --error ("bad comb case: " ++ prtm a ++ syn op ++ prtm b)

defn x  ds@(v:_) ts = let (&) = Let x in 
  [v&t | t<-ts] ++ [ d & last ts | d<-tail ds]

sep s = foldl1 (\x y->x++s++y)

calc t env = putStr . ('\n':) . sep "\n\n  =>  " $ map prtm $ reverse $ trace t env

test = calc t2 (\Z -> 2)


-- Samples and testing

(+:) = Bop Plus ;  (*:) = Bop Mult ;  (-:) = Bop Diff

x = Var X; y = Var Y; z = Var Z

t1 = x *: (x -: Lit 2)

t2 = Let X (Lit 5 *: Lit 3) (Let Y t1 ((x *: y) +: (z +: Lit 5)))





{-

------------------------
-- Variables updated "in-place"
-- idea: semantics is a trace, not of standard terms, but of
-- terms with (Var -> (Var+Int)) in place of vars

-- An alternate form of trace: UNDER DEVELOPMENT
-- Idea: trace' yields a function from subns to term-traces

trace' :: Eq c => Term Integer Oper c -> (c -> Term Integer Oper c) -> [Term Integer Oper c]
trace' = fold (\a     s -> [Lit a])
              (\o l r s -> comb o (l s) (r s))
              (\x d t s -> let ds@(v:_) = d s in
                           defn' x ds t s (set s x v))
              (\x     s -> [s x])

defn' x  ds@(v:_) ts s u = let (€) = Let x in 
  [t | t<-ts s] ++ [ d € last (ts u) | d<-ds]
              
calc' t sub = putStr . sep "\n\n  =>  " $ map prtm $ reverse $ trace' t sub

test' = calc' t2 (set Var Z (Lit 2))
-}