Make it possible to define things

With this change, the repl/evaluator now supports binding names to
values using a def form. We also endeavor to lookup the values of bound
names when encountered and carry context mutations across repl states.

Rose/Environment.idr

@@ -5,11 +5,13 @@ import Data.SExpression
 import Data.Vect
 
 ||| Assoc represents an associative structure.
+export
 interface Assoc (a: Type -> Type -> Type) where
   key   : a k v -> k
   value : a k v -> v
   assoc : k -> v -> a k v
 
+export
 Assoc Pair where
   key   = fst
   value = snd
@@ -52,38 +54,50 @@ getEnv (Local e) = e
 getEnv (Import e _) = e
 
 export
-record ExecutionContext (e: Type -> Type) (k: Type -> Type -> Type) (a: Type) (n: Nat) (m: Nat) where
+record ExecutionContext (e: Type -> Type) (k: Type -> Type -> Type) (a: Type) where
   constructor MkExecutionContext
   active   : Environment e k => Scope e k a
   global   : Environment e k => Scope e k a
-  imports  : Environment e k => Vect n (Scope e k a)
-  previous : Environment e k => Vect m (Scope e k a)
+  -- TODO: Change these to Vect if possible
+  imports  : Environment e k => List (Scope e k a)
+  previous : Environment e k => List (Scope e k a)
 
 export
-localScope : Environment e k => e (k a SE) -> ExecutionContext e k a n m -> ExecutionContext e k a n (S m)
+localScope : Environment e k => e (k a SE) -> ExecutionContext e k a -> ExecutionContext e k a
 localScope env p = MkExecutionContext (Local env) (global p) (imports p) $ (active p) :: (previous p)
 
 export
-importScope : Environment e k => e (k a SE) -> String -> ExecutionContext e k a n m -> ExecutionContext e k a (S n) m
+importScope : Environment e k => e (k a SE) -> String -> ExecutionContext e k a -> ExecutionContext e k a
 importScope e s p = MkExecutionContext (active p) (global p) ((Import e s) :: imports p) (previous p)
 
 export
-globalScope : Environment e k => e (k a SE) -> ExecutionContext e k a n m -> ExecutionContext e k a n m
+globalScope : Environment e k => e (k a SE) -> ExecutionContext e k a -> ExecutionContext e k a
 globalScope env p = MkExecutionContext (active p) (Local env) (imports p) (previous p)
 
 export
-pop : ExecutionContext e k a n (S m) -> ExecutionContext e k a n m
-pop c = MkExecutionContext (head (previous c)) (global c) (imports c) (tail (previous c))
+pop : (Environment e k, Alternative e) => ExecutionContext e k a -> ExecutionContext e k a
+pop c =
+  case tail' (previous c) of
+    Nothing => MkExecutionContext (Local empty) (global c) (imports c) (previous c)
+    Just t  => MkExecutionContext (fromMaybe (Local empty) (head' (previous c))) (global c) (imports c) t
 
 export
-resolveLocal : (Monoid a, Eq a, Environment e k) => ExecutionContext e k a n m -> a -> Maybe SE
+resolveLocal : (Monoid a, Eq a, Environment e k) => ExecutionContext e k a -> a -> Maybe SE
 resolveLocal c k = (lookup (getEnv (active c)) k)
                  <|> (foldl (<|>) Nothing (map ((flip lookup) k . getEnv) (previous c)))
 
 export
-resolveImport : (Monoid a, Eq a, Environment e k) => ExecutionContext e k a n m -> a -> Maybe SE
+resolveImport : (Monoid a, Eq a, Environment e k) => ExecutionContext e k a -> a -> Maybe SE
 resolveImport c k = foldl (<|>) Nothing (map ((flip lookup) k . getEnv) (imports c))
 
 export
-emptyContext : Alternative e => ExecutionContext e k a Z Z
+emptyContext : Alternative e => ExecutionContext e k a
 emptyContext = MkExecutionContext (Local empty) (Local empty) Nil Nil
+
+||| Add a new definition to the context's active environment.
+export
+define : (Environment e k, Assoc k, Monoid a, Eq a) => ExecutionContext e k a -> (k a SE) -> ExecutionContext e k a
+define ctx kv = let update = mutate (getEnv (active ctx)) kv
+                 in case update of
+                      Nothing  => ctx
+                      Just env => localScope env ctx

Rose/Evaluator.idr

@@ -14,83 +14,119 @@ import Data.SExpression
 import Data.Atom
 import Data.Form
 
+||| Concrete context definition we are currently using.
+export
+Context : Type
+Context = ExecutionContext List Pair String
+
+export
+builtInContext : Context
+builtInContext = emptyContext
+
 ||| EvaluationError generates an error from an un-evaluable s-expression.
-EvaluationError : SE -> ExecutionContext e k a n m -> RoseError
+EvaluationError : SE -> ExecutionContext e k a -> RoseError
 EvaluationError expr _ = MkError $ "Couldn't evaluate the form: " ++ show expr
 
 LetError : SE -> RoseError
 LetError expr = MkError $ "Bad let bindings: " ++ show expr
 
--- TODO: Define define.
---define : Environment -> SE -> (Either RoseError Environment)
---define env (Expression (MkAtom (MkSymbol name)) val) =
---  pure $ maybe ((name,val)::env) (\x => (name,val)::(delete (name,x) env)) (Lookup.lookup name env)
---define env _ = Left $ EvaluationError Nil
-
 ||| Evaluate an s-expression.
 export
-evaluate : ExecutionContext e k a n m -> SE -> (Either RoseError SE)
-evaluate env form = go form
+evaluate : (Context, SE) -> Either RoseError (Context, SE)
+evaluate (env, form) = go form
   where mutual
+        ||| Don't do anything to the environment, just return a new form
+        persist : Context -> SE -> Either RoseError (Context, SE)
+        persist env se = pure (env, se)
+
         ||| Force evaluation of a form.
-        evaluateEval : ExecutionContext e k a n m -> SE -> Either RoseError SE
+        evaluateEval : Context -> SE -> Either RoseError (Context, SE)
         evaluateEval env (Expression first Nil) =
-          evaluate env first >>= evaluate env
+          evaluate (env, first) >>= evaluate
 
         ||| Evaluate an if form (if true 1 2)
-        evaluateIf : ExecutionContext e k a n m -> SE -> SE -> SE -> Either RoseError SE
+        evaluateIf : Context -> SE -> SE -> SE -> Either RoseError (Context, SE)
         evaluateIf env condition true false =
-          (evaluate env condition)
-          >>= isBool
-          >>= \(MkAtom (MkBool b)) => if b then (evaluate env true) else (evaluate env false)
+          evaluate (env, condition)
+          >>= isBool . snd
+          >>= \(MkAtom (MkBool b)) => if b then (evaluate (env, true)) else (evaluate (env, false))
 
-        evaluatePrim : ExecutionContext e k a n m -> PrimitiveFunction -> SE -> SE -> Either RoseError SE
+        ||| Evaluate a builtin function
+        evaluatePrim : Context -> PrimitiveFunction -> SE -> SE -> Either RoseError (Context, SE)
         evaluatePrim env f a@(MkAtom x) (Expression b@(MkAtom y) Nil) =
           case f a b of
             Left e => Left e
-            x => x
+            Right x => pure (env, x)
         evaluatePrim env f a@(MkAtom x) other =
-          evaluate env other
-          >>= \r => case f a r of
-                      Left e => Left e
-                      x => x
+          evaluate (env, other)
+          >>= \(e, r) => case f a r of
+                        Left e => Left e
+                        Right x => pure (e, x)
         evaluatePrim env f x y =
-          evaluate env x
-          >>= \r => evaluate env y
-          >>= \n => case f r n of
+          evaluate (env, x)
+          >>= \(e, r) => evaluate (e, y)
+          >>= \(env', n) => case f r n of
                       Left e => Left e
-                      x => x
+                      Right x => pure (env', x)
 
-        go : SE -> (Either RoseError SE)
+        ||| Add a new definition to the current context
+        evaluateDefine : Context -> SE -> SE -> Either RoseError (Context, SE)
+        evaluateDefine env atm@(MkAtom (MkSymbol name)) value =
+          evaluate (env, value)
+          >>= \(ctx', v) => pure ((define ctx' (name, v)), Nil)
+        evaluateDefine env name value = Left $ EvaluationError (Expression name value) env
+
+        ||| Find a definition in the current context
+        resolveDefinition : Context -> String -> Either RoseError (Context, SE)
+        resolveDefinition ctx name = case resolveLocal ctx name of
+                                       Nothing => pure (ctx, Nil)
+                                       Just v  => pure (ctx, v)
+
+        go : SE -> Either RoseError (Context, SE)
+        -- Special symbolic forms
         go (ApplicationPat (MkAtom (MkSymbol "eval")) rest) = evaluateEval env rest
         go (ApplicationPat (MkAtom (MkSymbol "if")) (Expression condition (Expression true false))) =
           evaluateIf env condition true false
-        go (LetPat bindings body) = letTransform bindings body >>= evaluate env
-        go (LetRecPat bindings body) = letRec bindings body >>= evaluate env
-        go m@(MacroPat (Expression first rest) bod) = pure m
-        go f@(FunctionPat (Expression first rest) bod) = pure f
-        go (ApplicationPat m@(MacroPat _ _) e) = alpha 0 m >>= \r => beta r e
+        go (ApplicationPat (MkAtom (MkSymbol "def")) (Expression name value)) = evaluateDefine env name value
+
+        -- Base forms
+        go (LetPat bindings body) = letTransform bindings body >>= (persist env) >>= evaluate
+        go (LetRecPat bindings body) = letRec bindings body >>= (persist env) >>= evaluate
+        go m@(MacroPat (Expression first rest) bod) = persist env m
+        go f@(FunctionPat (Expression first rest) bod) = persist env f
+
+        -- Function application
+        go (ApplicationPat m@(MacroPat _ _) e) = alpha 0 m >>= \r => beta r e >>= persist env
         go (ApplicationPat f@(FunctionPat _ _) e) =
           (alpha 0 f)
           >>= \r => case (beta f e) of
                       Left _ => Left $ EvaluationError (Expression f e) env
-                      Right x => evaluate env x
-        go (ApplicationPat f Nil) = evaluate env f
+                      Right x => evaluate (env, x)
+        go (ApplicationPat f Nil) = evaluate (env, f)
         go (ApplicationPat a@(ApplicationPat _ _) rest@(Expression _ _)) =
-          (evaluate env) a
-          >>= \x => (evaluate env) rest
-          >>= \y => Apply x [y]
-          >>= evaluate env
-        go (ApplicationPat a@(ApplicationPat _ _) Nil) = evaluate env a
+          evaluate (env, a)
+          >>= \(e, x) => evaluate (e, rest)
+          >>= \(e', y) => case  Apply x [y] of
+                            Right s => pure (e', s)
+                            Left e => Left e
+          >>= evaluate
+        go (ApplicationPat a@(ApplicationPat _ _) Nil) = evaluate (env, a)
         go (ApplicationPat s@(MkAtom (MkSymbol st)) (Expression first rest)) =
           case getPrimitive st of
-            Nothing => Left $ EvaluationError Nil env
+            Nothing =>
+              case resolveDefinition env st of
+                Right (_, Nil) => Left $ EvaluationError Nil env
+                Right (ctx, v) => evaluate (ctx, (Expression v (Expression first rest)))
             Just f => evaluatePrim env f first rest
         go a@(ApplicationPat first rest) =
-          evaluate env first
-          >>= \evaled => evaluate env rest
-          >>= \r => pure (Expression evaled r)
-        go e@(Expression x Nil) = pure e
-        go a@(MkAtom x) = pure a
-        go Nil = pure Nil
+          evaluate (env, first)
+          >>= \(env', evaled) => evaluate (env', rest)
+          >>= \(e, r) => pure (e, (Expression evaled r))
+
+        -- Everything else
+        go exp@(Expression x Nil) = (persist env exp)
+        go atm@(MkAtom (MkSymbol x)) = resolveDefinition env x
+        go atm@(MkAtom x) = (persist env atm)
+        go Nil = (persist env Nil)
+
         go unknown = Left $ EvaluationError unknown env

Rose/Repl.idr

@@ -10,31 +10,31 @@ import Evaluator
 import Data.Error
 import Environment
 
-startingEnv : List (String, SE)
-startingEnv = empty
-
-startingContext : ExecutionContext List Pair String Z Z
-startingContext = emptyContext
-
-read : IO String
-read = getLine
+read : Context -> IO (Context, String)
+read ctx = getLine
   >>= (\x => pure (parse (list <|> array)
                    $ tokens
                    $ runLex x))
   >>= pure . go
-  where go : Either (ParseError (TokenData Token)) (SE, (List (TokenData Token))) -> String
-        go = either show (either show show . evaluate startingContext . fst)
+  where success : (Context, SE) -> (Context, String)
+        success (ctx', expr) = (ctx', show expr)
+
+        error : RoseError -> (Context, String)
+        error err = (ctx, show err)
+
+        go : Either (ParseError (TokenData Token)) (SE, (List (TokenData Token))) -> (Context, String)
+        go = either (\e => (ctx, show e)) (either error success . (\x => evaluate (ctx, x)) . fst)
 
-print : String -> IO ()
-print s = putStrLn s
+print : (Context, String) -> IO Context
+print (c, s) = putStrLn s >>= \_ => pure c
 
 main : IO ()
 main =
   putStrLn "Rose version 1.0"
   *> putStrLn "ctrl+c to exit"
-  *> loop
-  where loop : IO ()
-        loop = putStr "⚘: "
-               *> read
-               >>= putStrLn
-	       >>= \_ => loop
+  *> loop builtInContext
+  where loop : Context -> IO ()
+        loop ctx = putStr "⚘: "
+                 *> read ctx
+                 >>= print
+	         >>= loop