@@ -301,7 +301,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
301 -- assumed to be a global reference
301 -- assumed to be a global reference
302 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)
302 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)
304− specialMNs = [sMN 0 "__Unit", sMN 0 "__True", sMN 0 "__False"]
304+ specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"
306 -- dependencies of de bruijn variables are described in `bs'
306 -- dependencies of de bruijn variables are described in `bs'
307 getDepsTerm vs bs cd (V i) = (bs !! i) cd
307 getDepsTerm vs bs cd (V i) = (bs !! i) cd
@@ -377,9 +377,9 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
377 getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional
377 getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional
378 getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional
378 getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional
380− -- projections (= methods)
380+ -- projections
381+ getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n
381 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t
382 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t
382− -- getDepsTerm vs bs cd t -- TODO?
384 -- the easy cases
384 -- the easy cases
385 getDepsTerm vs bs cd (Constant _) = M.empty
385 getDepsTerm vs bs cd (Constant _) = M.empty