Fix defined vs free names confusion (fixes #22)

rzk/src/Rzk/Evaluator.hs

@@ -22,7 +22,6 @@ import           Control.Monad.Except
 import           Control.Monad.Reader
 import           Data.Functor.Identity
 import           Data.List             (nub, (\\))
-import           Data.Maybe            (isNothing)
 import           Data.Monoid           (Endo (..))
 import           Data.Text             (Text)
 import qualified Data.Text             as Text
@@ -52,10 +51,8 @@ ppEvalError = \case
 
 -- | Evaluation context.
 data Context var = Context
-  { contextDefinedVariables :: [(var, Term var)]
+  { contextDefinedVariables :: [(var, Maybe (Term var))]
     -- ^ Defined variables (variables that have terms assigned to them).
-  , contextFreeVariables    :: [var]
-    -- ^ Known free variables, used to avoid name clashes during substitution.
   , contextTopes            :: [Term var]
     -- ^ Topes in the context.
   , contextTopeInclusions   :: [(Term var, Term var)]
@@ -66,16 +63,19 @@ data Context var = Context
 emptyContext :: Context var
 emptyContext = Context
   { contextDefinedVariables = []
-  , contextFreeVariables = []
   , contextTopes = []
   , contextTopeInclusions = []
   }
 
 -- | Reassign term value to a variable.
-updateVar :: var -> Term var -> Context var -> Context var
-updateVar x t context@Context{..} = context
+updateVar' :: var -> Maybe (Term var) -> Context var -> Context var
+updateVar' x t context@Context{..} = context
   { contextDefinedVariables = (x, t) : contextDefinedVariables }
 
+-- | Reassign term value to a variable.
+updateVar :: var -> Term var -> Context var -> Context var
+updateVar x t = updateVar' x (Just t)
+
 -- | Reassign term value to a variable.
 removeVar :: Eq var => var -> Context var -> Context var
 removeVar x context@Context{..} = context
@@ -87,29 +87,24 @@ removeVar x context@Context{..} = context
 -- | Reassign term value to a variable.
 updateVars :: [(var, Term var)] -> Context var -> Context var
 updateVars xs context@Context{..} = context
-  { contextDefinedVariables = xs <> contextDefinedVariables }
+  { contextDefinedVariables = map (fmap Just) xs <> contextDefinedVariables }
 
 addVar :: var -> Context var -> Context var
-addVar x context@Context{..} = context
-  { contextFreeVariables = x : contextFreeVariables }
+addVar x = updateVar' x Nothing
 
 -- | List all known variables (used to avoid name clashes after substitution).
 contextKnownVars :: Context var -> [var]
-contextKnownVars Context{..} = contextFreeVariables <> map fst contextDefinedVariables
+contextKnownVars Context{..} = map fst contextDefinedVariables
 
 -- | Evaluation with variables of type @var@.
 newtype Eval var a = Eval { runEval :: ReaderT (Context var) (Except (EvalError var)) a }
   deriving (Functor, Applicative, Monad, MonadReader (Context var), MonadError (EvalError var))
 
 -- | Lookup definition of a variable (if exists).
 lookupVar :: Eq var => var -> Eval var (Maybe (Term var))
-lookupVar x = do
-  value <- asks (lookup x . contextDefinedVariables)
-  when (isNothing value) $ do
-    knownFreeVariable <- asks ((x `elem`) . contextFreeVariables)
-    when (not knownFreeVariable) $ do
-      throwError (EvalErrorUndefinedVariable x)
-  return value
+lookupVar x = asks (lookup x . contextDefinedVariables) >>= \case
+  Nothing -> throwError (EvalErrorUndefinedVariable x)
+  Just value -> return value
 
 -- | Add definition of a variable locally during evaluation.
 localVar :: MonadReader (Context var) m => (var, Term var) -> m a -> m a
@@ -131,7 +126,7 @@ enterScope
      MonadError (EvalError var) m, MonadReader (Context var) m)
   => (var, Term var) -> Term var -> (Term var -> m (f (Term var))) -> m (f (Term var))
 enterScope (x, e) body f = do
-  knownVars <- asks ((map fst . contextDefinedVariables) <> contextFreeVariables )
+  knownVars <- asks (map fst . contextDefinedVariables)
   let vars = knownVars ++ allVars body
       x' = refreshVar vars x
   localVar (x', e) $ do

rzk/src/Rzk/TypeChecker.hs

@@ -239,7 +239,8 @@ localTyping :: Eq var => (var, Maybe (Term var)) -> TypeCheck var a -> TypeCheck
 localTyping (x, t) m = do
   traverse_ (setTypeOf x) t
   oldContext <- get
-  result <- localFreeVar x (local (\context -> context { contextDefinedVariables = contextKnownHoles oldContext <> contextDefinedVariables context }) m)
+  result <- localFreeVar x (local (\context -> context
+    { contextDefinedVariables = map (fmap Just) (contextKnownHoles oldContext) <> contextDefinedVariables context }) m)
   traverse_ (unsetTypeOf x) t
   return result
 
@@ -663,7 +664,8 @@ ppContext Context{..} = Text.intercalate "\n"
   , Text.intercalate "\n" (map ppDef contextDefinedVariables)
   ]
     where
-      ppDef (x, t) = ppVar x <> " := " <> ppTerm t
+      ppDef (x, Nothing) = ppVar x <> " is a local variable"
+      ppDef (x, Just t)  = ppVar x <> " := " <> ppTerm t
 
 getTypeCheckResult :: Context var -> TypingContext var -> TypeCheck var () -> TypeCheckResult var
 getTypeCheckResult initialEvalContext initialTypingContext
@@ -686,8 +688,7 @@ typecheckModule freshVars Module{..} = do
       modify (\context -> context { contextKnownTypes = (declName, ty) : contextKnownTypes context})
   where
     initialEvalContext = Context
-      { contextDefinedVariables = map (\Decl{..} -> (declName, declBody)) moduleDecls
-      , contextFreeVariables = map declName moduleDecls
+      { contextDefinedVariables = map (\Decl{..} -> (declName, Just declBody)) moduleDecls
       , contextTopes = []
       , contextTopeInclusions = []
       }
@@ -1027,7 +1028,7 @@ unify term t1 t2 = localAction (ActionUnifyTypesFor term t1 t2) $ do
 
     -- unification by eta-expansion!
     unify'' (Lambda x a Nothing m) tt2 = do
-      vars <- asks contextFreeVariables
+      vars <- asks (map fst . contextDefinedVariables)
       let xs = freeVars x
           doRename = any (`elem` vars) xs
           xxs' = refreshVars (vars <> allVars m) xs
@@ -1039,7 +1040,7 @@ unify term t1 t2 = localAction (ActionUnifyTypesFor term t1 t2) $ do
           m' <- enterPatternScopeT (x, x') m evalType
           unify' m' (App tt2 x')
     unify'' tt1 (Lambda x a Nothing m) = do
-      vars <- asks contextFreeVariables
+      vars <- asks (map fst . contextDefinedVariables)
       let xs = freeVars x
           doRename = any (`elem` vars) xs
           xxs' = refreshVars (vars <> allVars m) xs
@@ -1051,7 +1052,7 @@ unify term t1 t2 = localAction (ActionUnifyTypesFor term t1 t2) $ do
           m' <- enterPatternScopeT (x, x') m evalType
           unify' (App tt1 x') m'
     unify'' (Lambda x a (Just phi) m) tt2 = do
-      vars <- asks contextFreeVariables
+      vars <- asks (map fst . contextDefinedVariables)
       let xs = freeVars x
           doRename = any (`elem` vars) xs
           xxs' = refreshVars (vars <> allVars m <> allVars phi) xs
@@ -1066,7 +1067,7 @@ unify term t1 t2 = localAction (ActionUnifyTypesFor term t1 t2) $ do
             let tt2' = App tt2 x'
             unify' tt1' tt2'
     unify'' tt1 (Lambda x a (Just phi) m) = do
-      vars <- asks contextFreeVariables
+      vars <- asks (map fst . contextDefinedVariables)
       let xs = freeVars x
           doRename = any (`elem` vars) xs
           xxs' = refreshVars (vars <> allVars m <> allVars phi) xs