git.iko.soy/Idris-dev
on master help sign in
Uniquify binder names when leaving executor
e7bd1f5David Raymond Christiansen
src/Idris/Core/Execute.hs+11−5
compare with master
unifiedsplit
@@ -51,8 +51,9 @@ readMay s = case reads s of
51
51
52data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
52data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
53
53
54−newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
54+data ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
55+ , binderNames :: [Name] -- ^ Used to uniquify binders when converting to TT
55− }
56+ }
56
57
57data ExecVal = EP NameType Name ExecVal
58data ExecVal = EP NameType Name ExecVal
58 | EV Int
59 | EV Int
@@ -80,9 +81,10 @@ instance Show ExecVal where
80toTT :: ExecVal -> Exec Term
81toTT :: ExecVal -> Exec Term
81toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
82toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
82toTT (EV i) = return $ V i
83toTT (EV i) = return $ V i
84+toTT (EBind n b body) = do n' <- newN n
83−toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
85+ body' <- body $ EP Bound n' EErased
84 b' <- fixBinder b
86 b' <- fixBinder b
85− Bind n b' <$> toTT body'
87+ Bind n' b' <$> toTT body'
86 where fixBinder (Lam t) = Lam <$> toTT t
88 where fixBinder (Lam t) = Lam <$> toTT t
87 fixBinder (Pi t k) = Pi <$> toTT t <*> toTT k
89 fixBinder (Pi t k) = Pi <$> toTT t <*> toTT k
88 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
90 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
92 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
94 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
93 fixBinder (PVar t) = PVar <$> toTT t
95 fixBinder (PVar t) = PVar <$> toTT t
94 fixBinder (PVTy t) = PVTy <$> toTT t
96 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'
95toTT (EApp e1 e2) = do e1' <- toTT e1
101toTT (EApp e1 e2) = do e1' <- toTT e1
96 e2' <- toTT e2
102 e2' <- toTT e2
97 return $ App e1' e2'
103 return $ App e1' e2'
@@ -115,7 +121,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args
115
121
116initState :: Idris ExecState
122initState :: Idris ExecState
117initState = do ist <- getIState
123initState = do ist <- getIState
118− return $ ExecState (idris_dynamic_libs ist)
124+ return $ ExecState (idris_dynamic_libs ist) []
119
125
120type Exec = ErrorT Err (StateT ExecState IO)
126type Exec = ErrorT Err (StateT ExecState IO)
121
127