@@ -51,8 +51,9 @@ readMay s = case reads s of
5151
5252data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
5353
54−newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
55− }
54+data ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
55+ , binderNames :: [Name] -- ^ Used to uniquify binders when converting to TT
56+ }
5657
5758data ExecVal = EP NameType Name ExecVal
5859 | EV Int
@@ -80,9 +81,10 @@ instance Show ExecVal where
8081toTT :: ExecVal -> Exec Term
8182toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
8283toTT (EV i) = return $ V i
83−toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
84+toTT (EBind n b body) = do n' <- newN n
85+ body' <- body $ EP Bound n' EErased
8486 b' <- fixBinder b
85− Bind n b' <$> toTT body'
87+ Bind n' b' <$> toTT body'
8688 where fixBinder (Lam t) = Lam <$> toTT t
8789 fixBinder (Pi t k) = Pi <$> toTT t <*> toTT k
8890 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
@@ -92,6 +94,10 @@ toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
9294 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
9395 fixBinder (PVar t) = PVar <$> toTT t
9496 fixBinder (PVTy t) = PVTy <$> toTT t
97+ newN n = do (ExecState hs ns) <- lift get
98+ let n' = uniqueName n ns
99+ lift (put (ExecState hs (n':ns)))
100+ return n'
95101toTT (EApp e1 e2) = do e1' <- toTT e1
96102 e2' <- toTT e2
97103 return $ App e1' e2'
@@ -115,7 +121,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args
115121
116122initState :: Idris ExecState
117123initState = do ist <- getIState
118− return $ ExecState (idris_dynamic_libs ist)
124+ return $ ExecState (idris_dynamic_libs ist) []
119125
120126type Exec = ErrorT Err (StateT ExecState IO)
121127